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

proof

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

end;

hence LattPOSet L is complete by LATTICE3:def 12; :: thesis: verum