let X be non empty set ; :: thesis: for Q being Subset of (FuzzyLattice X)
for x being Element of X holds ("\/" Q,(FuzzyLattice X)) . x = "\/" (pi Q,x),(RealPoset [.0 ,1.])
let Q be Subset of (FuzzyLattice X); :: thesis: for x being Element of X holds ("\/" Q,(FuzzyLattice X)) . x = "\/" (pi Q,x),(RealPoset [.0 ,1.])
let x be Element of X; :: thesis: ("\/" Q,(FuzzyLattice X)) . x = "\/" (pi Q,x),(RealPoset [.0 ,1.])
A1: for a being Element of X holds (X --> (RealPoset [.0 ,1.])) . a is complete LATTICE by FUNCOP_1:13;
FuzzyLattice X = (RealPoset [.0 ,1.]) |^ X by LFUZZY_0:def 4
.= product (X --> (RealPoset [.0 ,1.])) by YELLOW_1:def 5 ;
then (sup Q) . x = "\/" (pi Q,x),((X --> (RealPoset [.0 ,1.])) . x) by A1, WAYBEL_3:32;
hence ("\/" Q,(FuzzyLattice X)) . x = "\/" (pi Q,x),(RealPoset [.0 ,1.]) by FUNCOP_1:13; :: thesis: verum