let C be complete Lattice; :: thesis: for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)

let X be set ; :: thesis: "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)

set Y = { a where a is Element of C : a is_greater_than X } ;

A1: "\/" (X,C) is_less_than { a where a is Element of C : a is_greater_than X }

then "\/" (X,C) in { a where a is Element of C : a is_greater_than X } ;

then for b being Element of C st b is_less_than { a where a is Element of C : a is_greater_than X } holds

b [= "\/" (X,C) ;

hence "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) by A1, Th34; :: thesis: verum

let X be set ; :: thesis: "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)

set Y = { a where a is Element of C : a is_greater_than X } ;

A1: "\/" (X,C) is_less_than { a where a is Element of C : a is_greater_than X }

proof

X is_less_than "\/" (X,C)
by Def21;
let a be Element of C; :: according to LATTICE3:def 16 :: thesis: ( a in { a where a is Element of C : a is_greater_than X } implies "\/" (X,C) [= a )

assume a in { a where a is Element of C : a is_greater_than X } ; :: thesis: "\/" (X,C) [= a

then ex b being Element of C st

( a = b & b is_greater_than X ) ;

hence "\/" (X,C) [= a by Def21; :: thesis: verum

end;assume a in { a where a is Element of C : a is_greater_than X } ; :: thesis: "\/" (X,C) [= a

then ex b being Element of C st

( a = b & b is_greater_than X ) ;

hence "\/" (X,C) [= a by Def21; :: thesis: verum

then "\/" (X,C) in { a where a is Element of C : a is_greater_than X } ;

then for b being Element of C st b is_less_than { a where a is Element of C : a is_greater_than X } holds

b [= "\/" (X,C) ;

hence "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) by A1, Th34; :: thesis: verum