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

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