let C be complete Lattice; :: thesis: for X being set holds
( "\/" X,C = "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C & "/\" X,C = "/\" { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C )
let X be set ; :: thesis: ( "\/" X,C = "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C & "/\" X,C = "/\" { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C )
set Y = { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ;
set Z = { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ;
X is_less_than "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C

proof

let a be Element of C; :: according to LATTICE3:def 17 :: thesis: ( a in X implies a [= "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C )
assume a in X ; :: thesis: a [= "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C
then a in { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ;
hence a [= "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C by Th38; :: thesis: verum

end;

then A1: "\/" X,C [= "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C by Def21;
{ a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } is_less_than "\/" X,C

proof

let a be Element of C; :: according to LATTICE3:def 17 :: thesis: ( a in { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } implies a [= "\/" X,C )
assume a in { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ; :: thesis: a [= "\/" X,C
then ex b being Element of C st
( a = b & ex c being Element of C st
( b [= c & c in X ) ) ;
then consider c being Element of C such that
A2: a [= c and
A3: c in X ;
c [= "\/" X,C by A3, Th38;
hence a [= "\/" X,C by A2, LATTICES:25; :: thesis: verum

end;

then "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C [= "\/" X,C by Def21;
hence "\/" X,C = "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C by A1, LATTICES:26; :: thesis: "/\" X,C = "/\" { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C
X is_greater_than "/\" { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C

proof

let a be Element of C; :: according to LATTICE3:def 16 :: thesis: ( a in X implies "/\" { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C [= a )
assume a in X ; :: thesis: "/\" { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C [= a
then a in { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ;
hence "/\" { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C [= a by Th38; :: thesis: verum

end;

then A4: "/\" { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C [= "/\" X,C by Th34;
{ a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } is_greater_than "/\" X,C

proof

let a be Element of C; :: according to LATTICE3:def 16 :: thesis: ( a in { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } implies "/\" X,C [= a )
assume a in { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ; :: thesis: "/\" X,C [= a
then ex b being Element of C st
( a = b & ex c being Element of C st
( c [= b & c in X ) ) ;
then consider c being Element of C such that
A5: c [= a and
A6: c in X ;
"/\" X,C [= c by A6, Th38;
hence "/\" X,C [= a by A5, LATTICES:25; :: thesis: verum

end;

then "/\" X,C [= "/\" { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C by Th34;
hence "/\" X,C = "/\" { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C by A4, LATTICES:26; :: thesis: verum