let C be complete Lattice; :: thesis: for a being Element of C
for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C))
let a be Element of C; :: thesis: for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C))
let X be set ; :: thesis: "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (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_less_than a "/\" ("\/" (X,C))

proof

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

end;

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