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 z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9 ) )
take z = ((% x) "\/" (% y)) % ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9 ) )
A1: % x [= (% x) "\/" (% y) by LATTICES:5;
A2: % y [= (% y) "\/" (% x) by LATTICES:5;
A3: (% x) % = % x ;
A4: (% y) % = % y ;
hence ( x <= z & y <= z ) by A1, A2, A3, Th7; :: thesis: for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of (LattPOSet L); :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )
A5: (% z9) % = % z9 ;
assume that
A6: x <= z9 and
A7: y <= z9 ; :: thesis: z <= z9
A8: % x [= % z9 by A3, A5, A6, Th7;
% y [= % z9 by A4, A5, A7, Th7;
then (% x) "\/" (% y) [= % z9 by A8, FILTER_0:6;
hence z <= z9 by A5, 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 z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z ) )
take z = ((% x) "/\" (% y)) % ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z ) )
A9: (% x) "/\" (% y) [= % x by LATTICES:6;
A10: (% y) "/\" (% x) [= % y by LATTICES:6;
A11: (% x) % = % x ;
A12: (% y) % = % y ;
hence ( z <= x & z <= y ) by A9, A10, A11, Th7; :: thesis: for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of (LattPOSet L); :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )
A13: (% z9) % = % z9 ;
assume that
A14: z9 <= x and
A15: z9 <= y ; :: thesis: z9 <= z
A16: % z9 [= % x by A11, A13, A14, Th7;
% z9 [= % y by A12, A13, A15, Th7;
then % z9 [= (% x) "/\" (% y) by A16, FILTER_0:7;
hence z9 <= z by A13, Th7; :: thesis: verum