let L be non empty complete Poset; :: thesis: for X being set holds
( "\/" X,L = "\/" X,(latt L) & "/\" X,L = "/\" X,(latt L) )
let X be set ; :: thesis: ( "\/" X,L = "\/" X,(latt L) & "/\" X,L = "/\" X,(latt L) )
A1: RelStr(# the carrier of L,the InternalRel of L #) = LattPOSet (latt L) by LATTICE3:def 15;
then reconsider x = "\/" X,L as Element of (LattPOSet (latt L)) ;
reconsider y = "/\" X,(latt L) as Element of L by A1;

A2: now

let a be Element of L; :: thesis: ( a is_<=_than X implies a <= y )
reconsider a9 = a as Element of (LattPOSet (latt L)) by A1;
assume a is_<=_than X ; :: thesis: a <= y
then a9 is_<=_than X by A1, Th2;
then % a9 is_less_than X by LATTICE3:29;
then A3: % a9 [= "/\" X,(latt L) by LATTICE3:34;
(% a9) % = % a9 ;
then a9 <= ("/\" X,(latt L)) % by A3, LATTICE3:7;
hence a <= y by A1, Th1; :: thesis: verum

end;

ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) by LATTICE3:def 12;
then A4: ex_sup_of X,L by Th15;

A5: now

let a be Element of (latt L); :: thesis: ( X is_less_than a implies % x [= a )
reconsider a9 = a % as Element of L by A1;
assume X is_less_than a ; :: thesis: % x [= a
then X is_<=_than a % by LATTICE3:30;
then X is_<=_than a9 by A1, Th2;
then "\/" X,L <= a9 by A4, Def9;
then A6: x <= a % by A1, Th1;
(% x) % = % x ;
hence % x [= a by A6, LATTICE3:7; :: thesis: verum

end;

X is_<=_than "\/" X,L by A4, Def9;
then X is_<=_than x by A1, Th2;
then X is_less_than % x by LATTICE3:31;
hence "\/" X,L = "\/" X,(latt L) by A5, LATTICE3:def 21; :: thesis: "/\" X,L = "/\" X,(latt L)
"/\" X,(latt L) is_less_than X by LATTICE3:34;
then ("/\" X,(latt L)) % is_<=_than X by LATTICE3:28;
then A7: y is_<=_than X by A1, Th2;
then ex_inf_of X,L by A2, Th16;
hence "/\" X,L = "/\" X,(latt L) by A7, A2, Def10; :: thesis: verum