set A = {{}};
reconsider R = id {{}} as Relation of {{}} ;
reconsider R = R as Order of {{}} ;
take IT = RelStr(# {{}},R #); :: thesis: ( not IT is empty & IT is flat & IT is lower-bounded )
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 ( not IT is empty & IT is flat & IT is lower-bounded ) ; :: thesis: verum