let L be finite Lattice; :: thesis: ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a
the carrier of L c= the carrier of L ;
then reconsider L9 = the carrier of L as Subset of L ;
consider a being Element of (LattPOSet L) such that
A1: for b being Element of (LattPOSet L) st b in L9 holds
b <= a by Lm3;
for b being Element of (LattPOSet L) holds b <= a
proof
let b be Element of (LattPOSet L); :: 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 (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a ; :: thesis: verum