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 ;
hence a [= "\/" (X,C) by ; :: 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 ; :: 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 ;
hence "/\" (X,C) [= a by ; :: 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 ; :: thesis: verum