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