set S = "\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]);
"\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]) = @ ("\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) by LFUZZY_0:def 5;
hence "\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]) is RMembership_Func of X,X ; :: thesis: verum