let B be set ; :: thesis: for R being Rule
for t being object st B,R |- t holds
t in B \/ (rng R)
let R be Rule; :: thesis: for t being object st B,R |- t holds
t in B \/ (rng R)
let t be object ; :: thesis: ( B,R |- t implies t in B \/ (rng R) )
assume B,R |- t ; :: thesis: t in B \/ (rng R)
then consider P being B,R -correct Formula-sequence such that
A2: t in rng P ;
set X = B \/ (rng R);
consider b being object such that
A3: b in dom P and
A4: t = P . b by A2, FUNCT_1:def 3;
b in Seg (len P) by A3, FINSEQ_1:def 3;
then reconsider n = b as Nat ;
P is B,R -correct ;
then P,n is_a_correct_step_wrt B,R by A3;

per cases then ( P . n in B or ex Q being Formula-finset st
( [Q,(P . n)] in R & ( for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t ) ) ) ) ;

suppose P . n in B ; :: thesis: t in B \/ (rng R)

hence t in B \/ (rng R) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider Q being Formula-finset such that
A5: [Q,(P . n)] in R and
for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t ) ;
P . n in rng R by A5, XTUPLE_0:def 13;
hence t in B \/ (rng R) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;