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 object ; :: 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 (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { (([:X,X:],((@ r9) (#) (@ s9))) @) where s9 is Element of (FuzzyLattice [:X,X:]) : s9 in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } }
proof
deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" ( { (([:X,X:],((@ $1) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]));
deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" ( { ((@ $1) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]));
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
for r being Element of (FuzzyLattice [:X,X:]) holds "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : 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 (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))
proof
let r be Element of (FuzzyLattice [:X,X:]); :: thesis: "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : 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 (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))
{ ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } }
proof
deffunc H3( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ r) (#) (@ $1))) @ ;
deffunc H4( Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL:] = (@ r) (#) (@ $1);
defpred S2[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
A4: for s being Element of (FuzzyLattice [:X,X:]) holds H4(s) = H3(s) by LFUZZY_0:def 6;
{ H4(s) where s is Element of (FuzzyLattice [:X,X:]) : S2[s] } = { H3(s) where s is Element of (FuzzyLattice [:X,X:]) : S2[s] } from FRAENKEL:sch 5(A4);
 hence { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: verum
end;
hence "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : 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 (FuzzyLattice [:X,X:]) : 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 (FuzzyLattice [:X,X:]) holds H2(r) = H1(r) ;
{ H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch 5(A5);
 hence { ("\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { (([:X,X:],((@ r9) (#) (@ s9))) @) where s9 is Element of (FuzzyLattice [:X,X:]) : s9 in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: verum
end;
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
defpred S2[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
deffunc H1( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ $1) (#) (@ $2))) @ ;
A6: { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) 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 (FuzzyLattice [:X,X:]) : ( 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 object ; :: 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) ;
i iter R = ([:X,X:],(i iter R)) @ by LFUZZY_0:def 6;
then reconsider r = i iter R as Element of (FuzzyLattice [:X,X:]) ;
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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 H2( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL:] = (@ $1) (#) (@ $2);
deffunc H3( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ $1) (#) (@ $2))) @ ;
defpred S3[ Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])] 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 (FuzzyLattice [:X,X:]) holds H3(r,s) = H2(r,s) by LFUZZY_0:def 6;
{ H3(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S3[r,s] } = { H2(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S3[r,s] } from FRAENKEL:sch 7(A14);
 hence { (([:X,X:],((@ r) (#) (@ s))) @) where r, s is Element of (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : ( 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 (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } }
proof
set A = { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ;
set B = { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ;
thus { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } c= { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } :: according to XBOOLE_0:def 10 :: thesis: { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of (FuzzyLattice [:X,X:]) 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 (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) by A15, A1, A16, Th34;
hence a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } by A17; :: thesis: verum
end;
thus { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A18: a = "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : 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 (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } by A19; :: thesis: verum
end;
end;
hence (TrCl R) (#) (TrCl R) = "\/" ( { ("\/" ( { H1(r,s) where s is Element of (FuzzyLattice [:X,X:]) : S1[s] } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : S2[r] } ,(FuzzyLattice [:X,X:])) by A15, A1, A3, Th35
.= "\/" ( { H1(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : ( S2[r] & S1[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