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 ; :: according to LATTICE3:def 10 :: thesis: ex z being Element of st
( x <= z & y <= z & ( for z' being Element of st x <= z' & y <= z' holds
z <= z' ) )
take z = ((% x) "\/" (% y)) % ; :: thesis: ( x <= z & y <= z & ( for z' being Element of st x <= z' & y <= z' holds
z <= z' ) )
A1: % x [= (% x) "\/" (% y) by LATTICES:22;
A2: % y [= (% y) "\/" (% x) by LATTICES:22;
A3: (% x) % = % x ;
A4: (% y) % = % y ;
hence ( x <= z & y <= z ) by A1, A2, A3, Th7; :: thesis: for z' being Element of st x <= z' & y <= z' holds
z <= z'
let z' be Element of ; :: thesis: ( x <= z' & y <= z' implies z <= z' )
A5: (% z') % = % z' ;
assume that
A6: x <= z' and
A7: y <= z' ; :: thesis: z <= z'
A8: % x [= % z' by A3, A5, A6, Th7;
% y [= % z' by A4, A5, A7, Th7;
then (% x) "\/" (% y) [= % z' by A8, FILTER_0:6;
hence z <= z' by A5, Th7; :: thesis: verum

end;

let x, y be Element of ; :: according to LATTICE3:def 11 :: thesis: ex z being Element of st
( z <= x & z <= y & ( for z' being Element of st z' <= x & z' <= y holds
z' <= z ) )
take z = ((% x) "/\" (% y)) % ; :: thesis: ( z <= x & z <= y & ( for z' being Element of st z' <= x & z' <= y holds
z' <= z ) )
A9: (% x) "/\" (% y) [= % x by LATTICES:23;
A10: (% y) "/\" (% x) [= % y by LATTICES:23;
A11: (% x) % = % x ;
A12: (% y) % = % y ;
hence ( z <= x & z <= y ) by A9, A10, A11, Th7; :: thesis: for z' being Element of st z' <= x & z' <= y holds
z' <= z
let z' be Element of ; :: thesis: ( z' <= x & z' <= y implies z' <= z )
A13: (% z') % = % z' ;
assume that
A14: z' <= x and
A15: z' <= y ; :: thesis: z' <= z
A16: % z' [= % x by A11, A13, A14, Th7;
% z' [= % y by A12, A13, A15, Th7;
then % z' [= (% x) "/\" (% y) by A16, FILTER_0:7;
hence z' <= z by A13, Th7; :: thesis: verum