let P be non empty flat Poset; :: thesis: for K being non empty Chain of P ex a being Element of P st
( K = {a} or K = {(Bottom P),a} )
let K be non empty Chain of P; :: thesis: ex a being Element of P st
( K = {a} or K = {(Bottom P),a} )
set z = Bottom P;

per cases ( ex a being Element of K st a <> Bottom P or for a being Element of K holds not a <> Bottom P ) ;

suppose ex a being Element of K st a <> Bottom P ; :: thesis: ex a being Element of P st
( K = {a} or K = {(Bottom P),a} )

then consider a being Element of K such that
B1: a <> Bottom P ;
take a ; :: thesis: ( K = {a} or K = {(Bottom P),a} )
D1: for x being object holds
( not x in K or x = Bottom P or x = a )

proof

let x be object ; :: thesis: ( not x in K or x = Bottom P or x = a )
assume E1: x in K ; :: thesis: ( x = Bottom P or x = a )
then reconsider x = x as Element of P ;
( x <= a or a <= x ) by E1, RELAT_2:def 7, ORDERS_2:def 7;
hence ( x = Bottom P or x = a ) by Lemflat01, B1; :: thesis: verum

end;

( K = {a} or K = {(Bottom P),a} )

proof

per cases ( Bottom P in K or not Bottom P in K ) ;

suppose C1: Bottom P in K ; :: thesis: ( K = {a} or K = {(Bottom P),a} )

for x being object st ( x = Bottom P or x = a ) holds
x in K by C1;
hence ( K = {a} or K = {(Bottom P),a} ) by D1, TARSKI:def 2; :: thesis: verum

end;

suppose C2: not Bottom P in K ; :: thesis: ( K = {a} or K = {(Bottom P),a} )

D1: for x being object st x in K holds
x = a

proof

let x be object ; :: thesis: ( x in K implies x = a )
assume E1: x in K ; :: thesis: x = a
reconsider x = x as Element of P by E1;
( x <= a or a <= x ) by E1, RELAT_2:def 7, ORDERS_2:def 7;
hence x = a by B1, E1, C2, Lemflat01; :: thesis: verum

end;

for x being object st x = a holds
x in K ;
hence ( K = {a} or K = {(Bottom P),a} ) by D1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence ( K = {a} or K = {(Bottom P),a} ) ; :: thesis: verum

end;

suppose A1: for a being Element of K holds not a <> Bottom P ; :: thesis: ex a being Element of P st
( K = {a} or K = {(Bottom P),a} )

take Bottom P ; :: thesis: ( K = {(Bottom P)} or K = {(Bottom P),(Bottom P)} )
B1: for x being object st x in K holds
x = Bottom P by A1;
for x being object st x = Bottom P holds
x in K

proof

let x be object ; :: thesis: ( x = Bottom P implies x in K )
assume C1: x = Bottom P ; :: thesis: x in K
the Element of K = Bottom P by A1;
hence x in K by C1; :: thesis: verum

end;

hence ( K = {(Bottom P)} or K = {(Bottom P),(Bottom P)} ) by B1, TARSKI:def 1; :: thesis: verum

end;

end;