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