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

proof

take x = Top (LattPOSet L); :: thesis: x is_>=_than the carrier of (LattPOSet L)
consider z being Element of such that
A1: for v being Element of holds
( z "\/" v = z & v "\/" z = z ) by LATTICES:def 14;
reconsider z' = z as Element of ;
A2: z = Top L by A1, LATTICES:def 17;

A3: now

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

end;

z' is_<=_than {} by YELLOW_0:6;
then A5: z' = "/\" {} ,(LattPOSet L) by A3, YELLOW_0:31;

now

reconsider x' = x as Element of ;
let a be Element of ; :: 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 ;
Top (LattPOSet L) = Top L by A2, A5, YELLOW_0:def 12;
then A6: a' [= x' by LATTICES:45;
( a' % = a' & x' % = x' ) ;
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