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

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

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