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_{1}[ Nat] means R c= ;

A3: R c= by A1;

A4: for k being non zero Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[1]
by Th25;

for k being non zero Nat holds S_{1}[k]
from NAT_1:sch 10(A5, A4);

then S_{1}[n]
;

hence R c= ; :: thesis: verum

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

A3: R c= by A1;

A4: for k being non zero Nat st S

S

proof

A5:
S
let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then R (#) R c= by Th6;

then R (#) R c= by Th26;

hence S_{1}[k + 1]
by A3, Th5; :: thesis: verum

end;assume S

then R (#) R c= by Th6;

then R (#) R c= by Th26;

hence S

for k being non zero Nat holds S

then S

hence R c= ; :: thesis: verum