let L be complete Lattice; :: thesis: for X being set holds
( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) )
let X be set ; :: thesis: ( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) )
A1: now :: thesis: for r being Element of (LattPOSet L) st X is_<=_than r holds
("\/" (X,L)) % <= r
let r be Element of (LattPOSet L); :: thesis: ( X is_<=_than r implies ("\/" (X,L)) % <= r )
assume X is_<=_than r ; :: thesis: ("\/" (X,L)) % <= r
then X is_less_than % r by LATTICE3:31;
then A2: "\/" (X,L) [= % r by LATTICE3:def 21;
(% r) % = % r ;
hence ("\/" (X,L)) % <= r by A2, LATTICE3:7; :: thesis: verum
end;
X is_less_than "\/" (X,L) by LATTICE3:def 21;
then A3: X is_<=_than ("\/" (X,L)) % by LATTICE3:30;
then ex_sup_of X, LattPOSet L by A1, Th15;
hence "\/" (X,L) = "\/" (X,(LattPOSet L)) by A3, A1, Def9; :: thesis: "/\" (X,L) = "/\" (X,(LattPOSet L))
A4: now :: thesis: for r being Element of (LattPOSet L) st X is_>=_than r holds
("/\" (X,L)) % >= r
let r be Element of (LattPOSet L); :: thesis: ( X is_>=_than r implies ("/\" (X,L)) % >= r )
assume X is_>=_than r ; :: thesis: ("/\" (X,L)) % >= r
then X is_greater_than % r by LATTICE3:29;
then A5: % r [= "/\" (X,L) by LATTICE3:34;
(% r) % = % r ;
hence ("/\" (X,L)) % >= r by A5, LATTICE3:7; :: thesis: verum
end;
X is_greater_than "/\" (X,L) by LATTICE3:34;
then A6: X is_>=_than ("/\" (X,L)) % by LATTICE3:28;
then ex_inf_of X, LattPOSet L by A4, Th16;
hence "/\" (X,L) = "/\" (X,(LattPOSet L)) by A6, A4, Def10; :: thesis: verum