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]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y9 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]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y9 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]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y9 is Element of X : verum }
let x, z be Element of X; :: thesis: { ("\/" { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y9 is Element of X : verum }
set RP = RealPoset [.0 ,1.];
set FL = FuzzyLattice [:X,X:];
defpred S₁[ Element of X] means verum;
deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { ((R . [x,$1]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[$1,z] } ,(RealPoset [.0 ,1.]);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { ((R . [x,$1]) "/\" (r . [$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.]);
for y being Element of X holds "\/" { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])

proof

let y be Element of X; :: thesis: "\/" { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])
set A = { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ;
set B = { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
A1: { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } )
assume a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A2: a = (R . [x,y]) "/\" (r . [y,z]) and
A3: r in Q ;
r . [y,z] in pi Q,[y,z] by A3, CARD_3:def 6;
hence a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } by A2; :: thesis: verum

end;

{ ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } c= { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } or a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ; :: thesis: a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider b being Element of (RealPoset [.0 ,1.]) such that
A4: a = (R . [x,y]) "/\" b and
A5: b in pi Q,[y,z] ;
ex f being Function st
( f in Q & b = f . [y,z] ) by A5, CARD_3:def 6;
hence a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A4; :: thesis: verum

end;

hence "\/" { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.]) by A1, XBOOLE_0:def 10; :: thesis: verum

end;

then A6: for y being Element of X holds H₁(y) = H₂(y) ;
thus { H₁(y) where y is Element of X : S₁[y] } = { H₂(y) where y is Element of X : S₁[y] } from FRAENKEL:sch 5(A6); :: thesis: verum