let X be non empty set ; :: thesis: for f being Membership_Func of X holds f is Element of (FuzzyLattice X)
let f be Membership_Func of X; :: thesis: f is Element of (FuzzyLattice X)
( dom f = X & rng f c= [.0 ,1.] ) by FUNCT_2:def 1, RELAT_1:def 19;
then f in Funcs X,[.0 ,1.] by FUNCT_2:def 2;
hence f is Element of (FuzzyLattice X) by Th14; :: thesis: verum