let P be non empty flat Poset; :: thesis: for p1, p2 being Element of P holds
( p1 <= p2 iff ( p1 = Bottom P or p1 = p2 ) )
let p1, p2 be Element of P; :: thesis: ( p1 <= p2 iff ( p1 = Bottom P or p1 = p2 ) )
consider a being Element of P such that
A1: for x, y being Element of P holds
( x <= y iff ( x = a or x = y ) ) by Defflat;
a = Bottom P
proof
for x being Element of P holds a <= x by A1;
hence a = Bottom P by ThMin02, LemMin01; :: thesis: verum
end;
hence ( p1 <= p2 iff ( p1 = Bottom P or p1 = p2 ) ) by A1; :: thesis: verum