let A be RelStr ; ( A is empty implies ( A is reflexive & A is transitive & A is antisymmetric ) )
assume A1:
A is empty
; ( 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; verum