let B be set ; :: thesis:
let R be Rule; :: thesis:
let P be Formula-sequence; :: thesis:
let m, n be Nat; :: thesis:
assume that
A3: P,m is_a_correct_step_wrt B,R and
A4: m <= n and
A5: P . m = P . n ; :: thesis:

per cases by A3;

suppose P . m in B ; :: thesis:

hence P,n is_a_correct_step_wrt B,R by A5; :: thesis:

end;

suppose ex Q being Formula-finset st
( [Q,(P . m)] in R & ( for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < m & P . k = t ) ) ) ; :: thesis:

then consider Q being Formula-finset such that
A10: [Q,(P . m)] in R and
A11: for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < m & P . k = t ) ;
for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t )

proof

let t be object ; :: thesis:
assume t in Q ; :: thesis:
then consider k being Nat such that
A15: ( k in dom P & k < m & P . k = t ) by A11;
take k ; :: thesis:
thus ( k in dom P & k < n & P . k = t ) by A4, A15, XXREAL_0:2; :: thesis:

end;

hence P,n is_a_correct_step_wrt B,R by A5, A10; :: thesis:

end;

end;