let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for n being natural number st R is transitive & n > 0 holds
R c=
let R be RMembership_Func of X,X; :: thesis: for n being natural number st R is transitive & n > 0 holds
R c=
let n be natural number ; :: thesis: ( R is transitive & n > 0 implies R c= )
assume A1: ( R is transitive & n > 0 ) ; :: thesis: R c=
then A2: R c= by Def6;
defpred S₁[ Nat] means R c= ;
reconsider n = n as non empty Element of NAT by A1, ORDINAL1:def 13;
A3: S₁[1] by Th25;
A4: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty 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 A2, Th5; :: thesis: verum

end;

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