theorem Th35: :: LFUZZY_1:35

for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))