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, Def16;
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