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 & b in X ) ;
X is_less_than "\/" X,C by Def21;
then b [= "\/" X,C by A1, Def17;
hence c [= a "/\" ("\/" X,C) by A1, LATTICES:27; :: thesis: verum

end;

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