A formulation of an induction principle for diamond-free directed complete partial orders is proposed. This principle may be useful for specification and verification of non-discrete systems using interactive proof assistant software.