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) )
X is_less_than "\/" X,L by LATTICE3:def 21;
then A1: X is_<=_than ("\/" X,L) % by LATTICE3:30;

A2: 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 ( "\/" X,L [= % r & (% r) % = % r & % r = r ) by LATTICE3:def 21;
hence ("\/" X,L) % <= r by LATTICE3:7; :: thesis: verum

end;

then ex_sup_of X, LattPOSet L by A1, Th15;
hence "\/" X,L = "\/" X,(LattPOSet L) by A1, A2, Def9; :: thesis: "/\" X,L = "/\" X,(LattPOSet L)
X is_greater_than "/\" X,L by LATTICE3:34;
then A3: X is_>=_than ("/\" X,L) % by LATTICE3:28;

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 ( % r [= "/\" X,L & (% r) % = % r & % r = r ) by LATTICE3:34;
hence ("/\" X,L) % >= r by LATTICE3:7; :: thesis: verum

end;

then ex_inf_of X, LattPOSet L by A3, Th16;
hence "/\" X,L = "/\" X,(LattPOSet L) by A3, A4, Def10; :: thesis: verum