let IT be non empty discrete RelStr ; :: thesis: ( IT is trivial implies IT is flat )
assume A: IT is trivial ; :: thesis: IT is flat
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

take a = the Element of IT; :: thesis: ( a is_<=_than the carrier of IT & ( for x, y being Element of IT holds
( x <= y iff ( x = a or x = y ) ) ) )
for b being Element of IT st b in the carrier of IT holds
a <= b by A, STRUCT_0:def 10;
hence ( a is_<=_than the carrier of IT & ( for x, y being Element of IT holds
( x <= y iff ( x = a or x = y ) ) ) ) by STRUCT_0:def 10, A; :: thesis: verum

end;

hence IT is flat ; :: thesis: verum