let L be Lattice; :: thesis: ( LattPOSet L is with_suprema & LattPOSet L is with_infima )
thus LattPOSet L is with_suprema :: thesis: LattPOSet L is with_infima

proof

let x, y be Element of (LattPOSet L); :: according to LATTICE3:def 10 :: thesis: ex z being Element of (LattPOSet L) st
( x <= z & y <= z & ( for z' being Element of (LattPOSet L) st x <= z' & y <= z' holds
z <= z' ) )
take z = ((% x) "\/" (% y)) % ; :: thesis: ( x <= z & y <= z & ( for z' being Element of (LattPOSet L) st x <= z' & y <= z' holds
z <= z' ) )
A1: ( % x [= (% x) "\/" (% y) & % y [= (% y) "\/" (% x) & (% y) "\/" (% x) = (% x) "\/" (% y) & % x = x & (% x) % = % x & % y = y & (% y) % = % y ) by LATTICES:22;
hence ( x <= z & y <= z ) by Th7; :: thesis: for z' being Element of (LattPOSet L) st x <= z' & y <= z' holds
z <= z'
let z' be Element of (LattPOSet L); :: thesis: ( x <= z' & y <= z' implies z <= z' )
A2: ( % z' = z' & (% z') % = % z' ) ;
assume ( x <= z' & y <= z' ) ; :: thesis: z <= z'
then ( % x [= % z' & % y [= % z' ) by A1, A2, Th7;
then (% x) "\/" (% y) [= % z' by FILTER_0:6;
hence z <= z' by A2, Th7; :: thesis: verum

end;

let x, y be Element of (LattPOSet L); :: according to LATTICE3:def 11 :: thesis: ex z being Element of (LattPOSet L) st
( z <= x & z <= y & ( for z' being Element of (LattPOSet L) st z' <= x & z' <= y holds
z' <= z ) )
take z = ((% x) "/\" (% y)) % ; :: thesis: ( z <= x & z <= y & ( for z' being Element of (LattPOSet L) st z' <= x & z' <= y holds
z' <= z ) )
A3: ( (% x) "/\" (% y) [= % x & (% y) "/\" (% x) [= % y & (% y) "/\" (% x) = (% x) "/\" (% y) & % x = x & (% x) % = % x & % y = y & (% y) % = % y ) by LATTICES:23;
hence ( z <= x & z <= y ) by Th7; :: thesis: for z' being Element of (LattPOSet L) st z' <= x & z' <= y holds
z' <= z
let z' be Element of (LattPOSet L); :: thesis: ( z' <= x & z' <= y implies z' <= z )
A4: ( % z' = z' & (% z') % = % z' ) ;
assume ( z' <= x & z' <= y ) ; :: thesis: z' <= z
then ( % z' [= % x & % z' [= % y ) by A3, A4, Th7;
then % z' [= (% x) "/\" (% y) by FILTER_0:7;
hence z' <= z by A4, Th7; :: thesis: verum