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;
( dom a = X & rng a c= [.0 ,1.] ) by A1;
hence a is Membership_Func of X by FUZZY_1:def 1; :: thesis: verum