let X be non empty set ; :: thesis: for a being Element of (FuzzyLattice X) holds a is Membership_Func of X
let a be Element of (FuzzyLattice X); :: thesis: a is Membership_Func of X
a in the carrier of (FuzzyLattice X) ;
then a in Funcs X,[.0 ,1.] by Th14;
then consider f being Function such that
A1: ( a = f & dom f = X & rng f c= [.0 ,1.] ) by FUNCT_2:def 2;
reconsider a = a as PartFunc of X,[.0 ,1.] by A1, RELSET_1:11;
reconsider a = a as PartFunc of X,REAL by RELSET_1:17;
X: ( dom a = X & rng a c= [.0 ,1.] ) by A1;
then a is Function of X,REAL by FUNCT_2:def 1;
hence a is Membership_Func of X by X, RELAT_1:def 19; :: thesis: verum