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 A1: ex f being Function st
( a = f & dom f = X & rng f c= [.0,1.] ) by FUNCT_2:def 2;
then reconsider a = a as PartFunc of X,[.0,1.] by RELSET_1:4;
reconsider a = a as PartFunc of X,REAL by RELSET_1:7;
a is Function of X,REAL by A1, FUNCT_2:def 1;
hence a is Membership_Func of X ; :: thesis: verum