for X being set ex a being Element of (LattPOSet L) st
( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )

proof

let X be set ; :: thesis: ex a being Element of (LattPOSet L) st
( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
take a = "\/" (X,(LattPOSet L)); :: thesis: ( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
X is_less_than "\/" (X,L) by LATTICE3:def 21;
then X is_<=_than ("\/" (X,L)) % by LATTICE3:30;
hence X is_<=_than a by YELLOW_0:29; :: thesis: for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b
let b be Element of (LattPOSet L); :: thesis: ( X is_<=_than b implies a <= b )
reconsider b9 = b as Element of L ;
assume X is_<=_than b ; :: thesis: a <= b
then X is_<=_than b9 % ;
then X is_less_than b9 by LATTICE3:30;
then A1: "\/" (X,L) [= b9 by LATTICE3:def 21;
( ("\/" (X,L)) % = a & b9 % = b ) by YELLOW_0:29;
hence a <= b by A1, LATTICE3:7; :: thesis: verum

end;

hence LattPOSet L is complete ; :: thesis: verum