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)

( 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)

( 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)

( 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)

( 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

( "\/" (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

then A1:
"\/" (X,C) [= "\/" ( { a where a is Element of C : ex b being Element of C st
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;( 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

( 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

then
"\/" ( { a where a is Element of C : ex b being Element of C st
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;( 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

( 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

then A4:
"/\" ( { a where a is Element of C : ex b being Element of C st
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;( 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

( 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

then
"/\" (X,C) [= "/\" ( { a where a is Element of C : ex b being Element of C st
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;( 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

( 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