set A = {{}};
reconsider R = id {{}} as Relation of {{}} ;
reconsider R = R as Order of {{}} ;
take IT = RelStr(# {{}},R #); :: thesis: ( IT is strict & not IT is empty & IT is flat )
reconsider z = {} as Element of IT by TARSKI:def 1;
ex a being Element of IT st
( a is_<=_than the carrier of IT & ( for x, y being Element of IT holds
( x <= y iff ( x = a or x = y ) ) ) )

proof

b1: for x being Element of IT holds z <= x by TARSKI:def 1;
for x, y being Element of IT holds
( x <= y iff ( x = z or x = y ) ) by TARSKI:def 1;
hence ex a being Element of IT st
( a is_<=_than the carrier of IT & ( for x, y being Element of IT holds
( x <= y iff ( x = a or x = y ) ) ) ) by b1, LemMin01; :: thesis: verum

end;

hence ( IT is strict & not IT is empty & IT is flat ) ; :: thesis: verum