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 S1[ Element of X] means verum;
deffunc H1( 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 H2( 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 object ; :: 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 object ; :: 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 H1(y) = H2(y) ;
thus { H1(y) where y is Element of X : S1[y] } = { H2(y) where y is Element of X : S1[y] } from FRAENKEL:sch 5(A6); :: thesis: verum