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

for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))

let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))

let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))

set FL = FuzzyLattice [:X,X:];

set RP = RealPoset [.0,1.];

"\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def 5;

then reconsider F = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ;

for x, z being Element of X holds ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z)

for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))

let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))

let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))

set FL = FuzzyLattice [:X,X:];

set RP = RealPoset [.0,1.];

"\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def 5;

then reconsider F = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ;

for x, z being Element of X holds ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z)

proof

hence
(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
by Th2; :: thesis: verum
let x, z be Element of X; :: thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z)

A1: { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:])

.= F . (x,z) by A1, A22, A3, A5, A12, A14, A24, A17, Th32 ; :: thesis: verum

end;A1: { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:])

proof

A3:
{ (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) )

assume t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])

then consider r being Element of (FuzzyLattice [:X,X:]) such that

A2: t = (@ r) (#) R and

r in Q ;

([:X,X:],((@ r) (#) R)) @ = (@ r) (#) R by LFUZZY_0:def 6;

hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; :: thesis: verum

end;assume t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])

then consider r being Element of (FuzzyLattice [:X,X:]) such that

A2: t = (@ r) (#) R and

r in Q ;

([:X,X:],((@ r) (#) R)) @ = (@ r) (#) R by LFUZZY_0:def 6;

hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; :: thesis: verum

proof

A5:
{ ("\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(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 }
deffunc H_{1}( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,$1]) } ,(RealPoset [.0,1.]));

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

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

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

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

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

end;deffunc H

defpred S

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

proof

then A4:
for y being Element of X holds H
FuzzyLattice [:X,X:] =
(RealPoset [.0,1.]) |^ [:X,X:]
by LFUZZY_0:def 4

.= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def 5 ;

then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ;

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

pi (Q,[x,y]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7;

hence ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) by LFUZZY_0:15; :: thesis: verum

end;.= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def 5 ;

then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ;

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

pi (Q,[x,y]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7;

hence ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) by LFUZZY_0:15; :: thesis: verum

{ H

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

proof

A12:
"\/" ( { ("\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((r9 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
deffunc H_{1}( 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.]));

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

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

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

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

end;deffunc H

defpred S

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

proof

then A11:
for y being Element of X holds H
let y be Element of X; :: thesis: "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(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 = { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ;

set B = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;

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

end;set A = { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ;

set B = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;

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

proof

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

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

then consider r being Element of (FuzzyLattice [:X,X:]) such that

A7: a = (r . [x,y]) "/\" (R . [y,z]) and

A8: r in Q ;

r . [x,y] in pi (Q,[x,y]) by A8, CARD_3:def 6;

hence a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } by A7; :: thesis: verum

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

then consider r being Element of (FuzzyLattice [:X,X:]) such that

A7: a = (r . [x,y]) "/\" (R . [y,z]) and

A8: r in Q ;

r . [x,y] in pi (Q,[x,y]) by A8, CARD_3:def 6;

hence a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } by A7; :: thesis: verum

proof

hence
"\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))
by A6, XBOOLE_0:def 10; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } or a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )

assume a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ; :: 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

A9: a = b "/\" (R . [y,z]) and

A10: b in pi (Q,[x,y]) ;

ex f being Function st

( f in Q & b = f . [x,y] ) by A10, 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 A9; :: thesis: verum

end;assume a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ; :: 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

A9: a = b "/\" (R . [y,z]) and

A10: b in pi (Q,[x,y]) ;

ex f being Function st

( f in Q & b = f . [x,y] ) by A10, 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 A9; :: thesis: verum

thus { H

proof

A14:
{ ("\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { (((@ r9) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
deffunc H_{1}( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = ($2 . [x,$1]) "/\" (R . [$1,z]);

defpred S_{1}[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;

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

A13: for y being Element of X

for r being Element of (FuzzyLattice [:X,X:]) st S_{2}[y] & S_{1}[r] holds

H_{1}(y,r) = H_{1}(y,r)
;

thus "\/" ( { ("\/" ( { H_{1}(y,r) where r is Element of (FuzzyLattice [:X,X:]) : S_{1}[r] } ,(RealPoset [.0,1.]))) where y is Element of X : S_{2}[y] } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { H_{1}(y9,r9) where y9 is Element of X : S_{2}[y9] } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : S_{1}[r9] } ,(RealPoset [.0,1.]))
from LFUZZY_0:sch 5(A13); :: thesis: verum

end;defpred S

defpred S

A13: for y being Element of X

for r being Element of (FuzzyLattice [:X,X:]) st S

H

thus "\/" ( { ("\/" ( { H

proof

A17:
{ (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
deffunc H_{1}( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (((@ $1) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));

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

defpred S_{1}[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;

for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds

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

H_{2}(r) = H_{1}(r)
;

thus { H_{2}(r) where r is Element of (FuzzyLattice [:X,X:]) : S_{1}[r] } = { H_{1}(r) where r is Element of (FuzzyLattice [:X,X:]) : S_{1}[r] }
from FRAENKEL:sch 6(A16); :: thesis: verum

end;deffunc H

defpred S

for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds

"\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))

proof

then A16:
for r being Element of (FuzzyLattice [:X,X:]) st S
let r be Element of (FuzzyLattice [:X,X:]); :: thesis: ( r in Q implies "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) )

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

{ ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum }

end;assume r in Q ; :: thesis: "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))

{ ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum }

proof

hence
"\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))
; :: thesis: verum
deffunc H_{3}( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ r) . [x,$1]) "/\" (R . [$1,z]);

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

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

A15: for y being Element of X holds H_{4}(y) = H_{3}(y)
by LFUZZY_0:def 5;

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

end;deffunc H

defpred S

A15: for y being Element of X holds H

thus { H

H

thus { H

proof

A22:
{ (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum }
set A = { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;

set B = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]);

thus { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def 10 :: thesis: pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

end;set B = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]);

thus { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def 10 :: thesis: pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

thus
pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
:: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) )

assume a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])

then consider r being Element of (FuzzyLattice [:X,X:]) such that

A18: a = ((@ r) (#) R) . [x,z] and

A19: r in Q ;

(@ r) (#) R in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A19;

hence a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A18, CARD_3:def 6; :: thesis: verum

end;assume a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])

then consider r being Element of (FuzzyLattice [:X,X:]) such that

A18: a = ((@ r) (#) R) . [x,z] and

A19: r in Q ;

(@ r) (#) R in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A19;

hence a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A18, CARD_3:def 6; :: thesis: verum

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) or b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )

assume b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; :: thesis: b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

then consider f being Function such that

A20: f in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and

A21: b = f . [x,z] by CARD_3:def 6;

ex r being Element of (FuzzyLattice [:X,X:]) st

( f = (@ r) (#) R & r in Q ) by A20;

hence b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21; :: thesis: verum

end;assume b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; :: thesis: b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

then consider f being Function such that

A20: f in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and

A21: b = f . [x,z] by CARD_3:def 6;

ex r being Element of (FuzzyLattice [:X,X:]) st

( f = (@ r) (#) R & r in Q ) by A20;

hence b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21; :: thesis: verum

proof

A24:
{ ("\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { (((@ r9) (#) R) . [x,z]) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
deffunc H_{1}( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,$1])),(RealPoset [.0,1.]))) "/\" (R . [$1,z]);

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

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

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

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

end;deffunc H

defpred S

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

proof

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

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

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

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

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

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

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

thus { H

proof

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

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

defpred S_{1}[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;

A25: for r being Element of (FuzzyLattice [:X,X:]) st S_{1}[r] holds

H_{2}(r) = H_{1}(r)
by Lm6;

thus { H_{2}(r) where r is Element of (FuzzyLattice [:X,X:]) : S_{1}[r] } = { H_{1}(r) where r is Element of (FuzzyLattice [:X,X:]) : S_{1}[r] }
from FRAENKEL:sch 6(A25); :: thesis: verum

end;deffunc H

defpred S

A25: for r being Element of (FuzzyLattice [:X,X:]) st S

H

thus { H

.= F . (x,z) by A1, A22, A3, A5, A12, A14, A24, A17, Th32 ; :: thesis: verum