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 }

proof

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;

X is_less_than "\/" X,C by Def21;
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 by Def16;
hence "\/" X,C = "/\" { a where a is Element of C : a is_greater_than X } ,C by A1, Th34; :: thesis: verum