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 that
A1: the InternalRel of r is_reflexive_in the carrier of r and
A2: ( the InternalRel of r is antisymmetric & the InternalRel of r is transitive ) ; :: thesis: ( r is reflexive & r is antisymmetric & r is transitive )
A3: the InternalRel of r is_transitive_in field the InternalRel of r by A2;
A4: field the InternalRel of r = the carrier of r by A1, PARTIT_2:21;
then the InternalRel of r is_antisymmetric_in the carrier of r by A2;
hence ( r is reflexive & r is antisymmetric & r is transitive ) by A1, A4, A3, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum