let X be non empty set ; :: thesis: for R being RMembership_Func of X,X

for Q being Subset of (FuzzyLattice [:X,X:])

for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:])

for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

let x, z be Element of X; :: thesis: { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

defpred S_{1}[ Element of X] means verum;

deffunc H_{1}( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . (x,$1)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . ($1,z));

deffunc H_{2}( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ("\/" ((pi (Q,[$1,z])),(RealPoset [.0,1.])));

for y being Element of X holds (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))_{1}(y) = H_{2}(y)
;

thus { H_{1}(y) where y is Element of X : S_{1}[y] } = { H_{2}(y9) where y9 is Element of X : S_{1}[y9] }
from FRAENKEL:sch 5(A1); :: thesis: verum

for Q being Subset of (FuzzyLattice [:X,X:])

for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:])

for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

let x, z be Element of X; :: thesis: { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }

defpred S

deffunc H

deffunc H

for y being Element of X holds (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))

proof

then A1:
for y being Element of X holds H
let y be Element of X; :: thesis: (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))

(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z] = ("\/" (Q,(FuzzyLattice [:X,X:]))) . [y,z] by LFUZZY_0:def 5

.= "\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])) by Th32 ;

hence (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) ; :: thesis: verum

end;(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z] = ("\/" (Q,(FuzzyLattice [:X,X:]))) . [y,z] by LFUZZY_0:def 5

.= "\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])) by Th32 ;

hence (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) ; :: thesis: verum

thus { H