let L be Lattice; ( LattPOSet L is with_suprema & LattPOSet L is with_infima )
thus
LattPOSet L is with_suprema
LattPOSet L is with_infima proof
let x,
y be
Element of
(LattPOSet L);
LATTICE3:def 10 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)) % ;
( 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;
for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9
let z9 be
Element of
(LattPOSet L);
( x <= z9 & y <= z9 implies z <= z9 )
A5:
(% z9) % = % z9
;
assume that A6:
x <= z9
and A7:
y <= z9
;
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;
verum
end;
let x, y be Element of (LattPOSet L); LATTICE3:def 11 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)) % ; ( 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; for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of (LattPOSet L); ( z9 <= x & z9 <= y implies z9 <= z )
A13:
(% z9) % = % z9
;
assume that
A14:
z9 <= x
and
A15:
z9 <= y
; 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; verum