let A be RelStr ; :: thesis: ( A is empty implies ( A is reflexive & A is transitive & A is antisymmetric ) )

assume A1: A is empty ; :: thesis: ( A is reflexive & A is transitive & A is antisymmetric )

then for x, y, z being object st x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in the InternalRel of A & [y,z] in the InternalRel of A holds

[x,z] in the InternalRel of A ;

then A2: the InternalRel of A is_transitive_in the carrier of A by RELAT_2:def 8;

for x, y being object st x in the carrier of A & y in the carrier of A & [x,y] in the InternalRel of A & [y,x] in the InternalRel of A holds

x = y by A1;

then A3: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 4;

for x being object st x in the carrier of A holds

[x,x] in the InternalRel of A by A1;

then the InternalRel of A is_reflexive_in the carrier of A by RELAT_2:def 1;

hence ( A is reflexive & A is transitive & A is antisymmetric ) by A2, A3, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum

assume A1: A is empty ; :: thesis: ( A is reflexive & A is transitive & A is antisymmetric )

then for x, y, z being object st x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in the InternalRel of A & [y,z] in the InternalRel of A holds

[x,z] in the InternalRel of A ;

then A2: the InternalRel of A is_transitive_in the carrier of A by RELAT_2:def 8;

for x, y being object st x in the carrier of A & y in the carrier of A & [x,y] in the InternalRel of A & [y,x] in the InternalRel of A holds

x = y by A1;

then A3: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 4;

for x being object st x in the carrier of A holds

[x,x] in the InternalRel of A by A1;

then the InternalRel of A is_reflexive_in the carrier of A by RELAT_2:def 1;

hence ( A is reflexive & A is transitive & A is antisymmetric ) by A2, A3, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum