let O be non empty OrthoRelStr ; :: thesis: ( O is StrictPartialOrdered implies O is irreflexive )
set IntRel = the InternalRel of O;
set CO = the carrier of O;
assume O is StrictPartialOrdered ; :: thesis: O is irreflexive
then A1: the InternalRel of O is irreflexive by Def11;
field the InternalRel of O c= the carrier of O \/ the carrier of O by RELSET_1:19;
then the InternalRel of O is_irreflexive_in the carrier of O by A1, Th16;
hence O is irreflexive by Def12; :: thesis: verum