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 S₁[ Nat] means R c= ;
A3: R c= by A1;
A4: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then R (#) R c= by Th6;
then R (#) R c= by Th26;
hence S₁[k + 1] by A3, Th5; :: thesis: verum

end;

A5: S₁[1] by Th25;
for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A5, A4);
then S₁[n] ;
hence R c= ; :: thesis: verum