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

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