ex x being Element of (LattPOSet L) st x is_>=_than the carrier of (LattPOSet L)

proof

consider z being Element of L such that
A1: for v being Element of L holds
( z "\/" v = z & v "\/" z = z ) by LATTICES:def 14;
reconsider z' = z as Element of (LattPOSet L) ;
A2: z' is_<=_than {} by YELLOW_0:6;
A3: z = Top L by A1, LATTICES:def 17;

now

let b' be Element of (LattPOSet L); :: thesis: ( b' is_<=_than {} implies z' >= b' )
reconsider b = b' as Element of L ;
assume b' is_<=_than {} ; :: thesis: z' >= b'
A4: ( b % = b & z % = z ) ;
b [= z by A3, LATTICES:45;
hence z' >= b' by A4, LATTICE3:7; :: thesis: verum

end;

then A5: z' = "/\" {} ,(LattPOSet L) by A2, YELLOW_0:31;
take x = Top (LattPOSet L); :: thesis: x is_>=_than the carrier of (LattPOSet L)

now

let a be Element of (LattPOSet L); :: thesis: ( a in the carrier of (LattPOSet L) implies a <= x )
assume a in the carrier of (LattPOSet L) ; :: thesis: a <= x
reconsider a' = a as Element of L ;
reconsider x' = x as Element of L ;
A6: ( a' % = a' & x' % = x' ) ;
Top (LattPOSet L) = Top L by A3, A5, YELLOW_0:def 12;
then a' [= x' by LATTICES:45;
hence a <= x by A6, LATTICE3:7; :: thesis: verum

end;

hence x is_>=_than the carrier of (LattPOSet L) by LATTICE3:def 9; :: thesis: verum

end;

hence LattPOSet L is upper-bounded by YELLOW_0:def 5; :: thesis: verum