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 :: thesis: for a being Element of L st a is_<=_than X holds
a <= y
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; :: 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 :: thesis: for a being Element of (latt L) st X is_less_than a holds
% x [= a
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;
(% 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