let L be finite Lattice; :: thesis: ex a being Element of st
for b being Element of holds b <= a
the carrier of L c= the carrier of L ;
then reconsider L' = the carrier of L as Subset of ;
consider a being Element of such that
A1: for b being Element of st b in L' holds
b <= a by Lm3;
for b being Element of holds b <= a

proof

let b be Element of ; :: thesis: b <= a
LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def 2;
hence b <= a by A1; :: thesis: verum

end;

hence ex a being Element of st
for b being Element of holds b <= a ; :: thesis: verum