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

proof

let c be Element of C; :: according to LATTICE3:def 16 :: thesis: ( c in { (a "\/" b) where b is Element of C : b in X } implies a "\/" ("/\" (X,C)) [= c )
assume c in { (a "\/" b) where b is Element of C : b in X } ; :: thesis: a "\/" ("/\" (X,C)) [= c
then consider b being Element of C such that
A1: c = a "\/" b and
A2: b in X ;
X is_greater_than "/\" (X,C) by Th34;
then "/\" (X,C) [= b by A2;
hence a "\/" ("/\" (X,C)) [= c by A1, FILTER_0:1; :: thesis: verum

end;

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