let r be non empty RelStr ; :: thesis: ( the InternalRel of r is_reflexive_in the carrier of r & the InternalRel of r is antisymmetric & the InternalRel of r is transitive implies ( r is reflexive & r is antisymmetric & r is transitive ) )
set i = the InternalRel of r;
set c = the carrier of r;
assume A1: ( the InternalRel of r is_reflexive_in the carrier of r & the InternalRel of r is antisymmetric & the InternalRel of r is transitive ) ; :: thesis: ( r is reflexive & r is antisymmetric & r is transitive )
then A2: field the InternalRel of r = the carrier of r by OPOSET_1:7;
then A3: the InternalRel of r is_antisymmetric_in the carrier of r by A1, RELAT_2:def 12;
the InternalRel of r is_transitive_in field the InternalRel of r by A1, RELAT_2:def 16;
hence ( r is reflexive & r is antisymmetric & r is transitive ) by A1, A2, A3, ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6; :: thesis: verum