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

proof

take x = Bottom (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 13;
reconsider z9 = z as Element of (LattPOSet L) ;
A2: z = Bottom L by A1, LATTICES:def 16;

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 ) ;
z [= b by A2, LATTICES:16;
hence z9 <= b9 by A4, LATTICE3:7; :: thesis: verum

end;

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

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

reconsider x9 = x as Element of L ;
let a be Element of (LattPOSet L); :: thesis: ( a in the carrier of (LattPOSet L) implies x <= a )
assume a in the carrier of (LattPOSet L) ; :: thesis: x <= a
reconsider a9 = a as Element of L ;
Bottom (LattPOSet L) = Bottom L by A2, A5, YELLOW_0:def 11;
then A6: x9 [= a9 by LATTICES:16;
( a9 % = a9 & x9 % = x9 ) ;
hence x <= a by A6, LATTICE3:7; :: thesis: verum

end;

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

end;

hence LattPOSet L is lower-bounded by YELLOW_0:def 4; :: thesis: verum