let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])
let R be RMembership_Func of X,X; :: thesis: (TrCl R) (#) (TrCl R) = "\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set FL = FuzzyLattice [:X,X:];
A1: { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (n iter R) where n is Element of NAT : n > 0 } or q in the carrier of (FuzzyLattice [:X,X:]) )
assume q in { (n iter R) where n is Element of NAT : n > 0 } ; :: thesis: q in the carrier of (FuzzyLattice [:X,X:])
then consider i being Element of NAT such that
A2: q = i iter R and
i > 0 ;
[:X,X:],(i iter R) @ = i iter R by LFUZZY_0:def 6;
hence q in the carrier of (FuzzyLattice [:X,X:]) by A2; :: thesis: verum

end;

A3: { ("\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" { ([:X,X:],((@ r') (#) (@ s')) @ ) where s' is Element of : s' in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } }

proof

deffunc H₁( Element of ) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ $1) (#) (@ s)) @ ) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]);
deffunc H₂( Element of ) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" { ((@ $1) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]);
defpred S₁[ Element of ] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
for r being Element of holds "\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])

proof

let r be Element of ; :: thesis: "\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])
{ ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } = { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } }

proof

deffunc H₃( Element of ) -> Element of the carrier of (FuzzyLattice [:X,X:]) = [:X,X:],((@ r) (#) (@ $1)) @ ;
deffunc H₄( Element of ) -> Element of bool [:[:X,X:],REAL :] = (@ r) (#) (@ $1);
defpred S₂[ Element of ] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
A4: for s being Element of holds H₄(s) = H₃(s) by LFUZZY_0:def 6;
{ H₄(s) where s is Element of : S₂[s] } = { H₃(s) where s is Element of : S₂[s] } from FRAENKEL:sch 5(A4);
hence { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } = { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: verum

end;

hence "\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) ; :: thesis: verum

end;

then A5: for r being Element of holds H₂(r) = H₁(r) ;
{ H₂(r) where r is Element of : S₁[r] } = { H₁(r) where r is Element of : S₁[r] } from FRAENKEL:sch 5(A5);
hence { ("\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" { ([:X,X:],((@ r') (#) (@ s')) @ ) where s' is Element of : s' in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: verum

end;

defpred S₁[ Element of ] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
defpred S₂[ Element of ] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
deffunc H₁( Element of , Element of ) -> Element of the carrier of (FuzzyLattice [:X,X:]) = [:X,X:],((@ $1) (#) (@ $2)) @ ;
A6: { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) }

proof

set A = { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ;
set B = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ;
thus { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } c= { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } :: according to XBOOLE_0:def 10 :: thesis: { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } or a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } )
assume a in { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; :: thesis: a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) }
then consider r, s being Element of such that
A7: a = (@ r) (#) (@ s) and
A8: ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) ;
A9: ( r = @ r & s = @ s ) by LFUZZY_0:def 5;
( ex i being Element of NAT st
( r = i iter R & i > 0 ) & ex j being Element of NAT st
( s = j iter R & j > 0 ) ) by A8;
hence a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } by A7, A9; :: thesis: verum

end;

thus { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } or b in { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } )
assume b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; :: thesis: b in { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }
then consider i, j being Element of NAT such that
A10: b = (i iter R) (#) (j iter R) and
A11: ( i > 0 & j > 0 ) ;
j iter R = [:X,X:],(j iter R) @ by LFUZZY_0:def 6;
then reconsider s = j iter R as Element of ;
i iter R = [:X,X:],(i iter R) @ by LFUZZY_0:def 6;
then reconsider r = i iter R as Element of ;
A12: ( @ r = r & @ s = s ) by LFUZZY_0:def 5;
( i iter R in { (n iter R) where n is Element of NAT : n > 0 } & j iter R in { (n iter R) where n is Element of NAT : n > 0 } ) by A11;
hence b in { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } by A10, A12; :: thesis: verum

end;

end;

A13: { ([:X,X:],((@ r) (#) (@ s)) @ ) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }

proof

deffunc H₂( Element of , Element of ) -> Element of bool [:[:X,X:],REAL :] = (@ $1) (#) (@ $2);
deffunc H₃( Element of , Element of ) -> Element of the carrier of (FuzzyLattice [:X,X:]) = [:X,X:],((@ $1) (#) (@ $2)) @ ;
defpred S₃[ Element of , Element of ] means ( $1 in { (n iter R) where n is Element of NAT : n > 0 } & $2 in { (n iter R) where n is Element of NAT : n > 0 } );
A14: for r, s being Element of holds H₃(r,s) = H₂(r,s) by LFUZZY_0:def 6;
{ H₃(r,s) where r, s is Element of : S₃[r,s] } = { H₂(r,s) where r, s is Element of : S₃[r,s] } from FRAENKEL:sch 7(A14);
hence { ([:X,X:],((@ r) (#) (@ s)) @ ) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; :: thesis: verum

end;

A15: "\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]) = @ ("\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) by LFUZZY_0:def 5;
{ ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } }

proof

set A = { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } ;
set B = { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } ;
thus { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } c= { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } :: according to XBOOLE_0:def 10 :: thesis: { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of such that
A16: a = (@ r) (#) (TrCl R) and
A17: r in { (n iter R) where n is Element of NAT : n > 0 } ;
a = "\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) by A15, A1, A16, Th34;
hence a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } by A17; :: thesis: verum

end;

thus { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of : r' in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: a in { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of such that
A18: a = "\/" { ((@ r) (#) (@ s)) where s is Element of : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) and
A19: r in { (n iter R) where n is Element of NAT : n > 0 } ;
a = (@ r) (#) (TrCl R) by A15, A1, A18, Th34;
hence a in { ((@ r) (#) (TrCl R)) where r is Element of : r in { (n iter R) where n is Element of NAT : n > 0 } } by A19; :: thesis: verum

end;

end;

hence (TrCl R) (#) (TrCl R) = "\/" { ("\/" { H₁(r,s) where s is Element of : S₁[s] } ,(FuzzyLattice [:X,X:])) where r is Element of : S₂[r] } ,(FuzzyLattice [:X,X:]) by A15, A1, A3, Th35
.= "\/" { H₁(r,s) where r, s is Element of : ( S₂[r] & S₁[s] ) } ,(FuzzyLattice [:X,X:]) from LFUZZY_0:sch 1()
.= "\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:]) by A6, A13 ;
:: thesis: verum