let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for n being Nat st R is transitive & n > 0 holds
R c=
let R be RMembership_Func of X,X; :: thesis: for n being Nat st R is transitive & n > 0 holds
R c=
let n be Nat; :: thesis: ( R is transitive & n > 0 implies R c= )
assume that
A1: R is transitive and
A2: n > 0 ; :: thesis: R c=
reconsider n = n as non zero Element of NAT by A2, ORDINAL1:def 12;
defpred S1[ Nat] means R c= ;
A3: R c= by A1;
A4: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then R (#) R c= by Th6;
then R (#) R c= by Th26;
hence S1[k + 1] by A3, Th5; :: thesis: verum
end;
A5: S1[1] by Th25;
for k being non zero Nat holds S1[k] from NAT_1:sch 10(A5, A4);
 then S1[n] ;
hence R c= ; :: thesis: verum