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:7; :: 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:8; :: 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:7; :: 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:8; :: thesis: verum