ex x being Element of (LattPOSet L) 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 L such that
A1: for v being Element of L holds
( z "\/" v = z & v "\/" z = z ) by LATTICES:def 14;
reconsider z9 = z as Element of (LattPOSet L) ;
A2: z = Top L by A1, LATTICES:def 17;

A3: now :: thesis: for b9 being Element of (LattPOSet L) st b9 is_<=_than {} holds
z9 >= b9

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

end;

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

now :: thesis: for a being Element of (LattPOSet L) st a in the carrier of (LattPOSet L) holds
a <= x

reconsider x9 = x as Element of L ;
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 a9 = a as Element of L ;
Top (LattPOSet L) = Top L by A2, A5, YELLOW_0:def 12;
then A6: a9 [= x9 by LATTICES:19;
( a9 % = a9 & x9 % = x9 ) ;
hence a <= x by A6, LATTICE3:7; :: thesis: verum

end;

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

end;

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