let B be set ; :: thesis: for R being Rule
for a being object holds
( not B,R |- a or a in B or ex S being Formula-finset st
( [S,a] in R & ( for b being object st b in S holds
B,R |- b ) ) )
let R be Rule; :: thesis: for a being object holds
( not B,R |- a or a in B or ex S being Formula-finset st
( [S,a] in R & ( for b being object st b in S holds
B,R |- b ) ) )
let a be object ; :: thesis: ( not B,R |- a or a in B or ex S being Formula-finset st
( [S,a] in R & ( for b being object st b in S holds
B,R |- b ) ) )
assume that
A1: B,R |- a and
A2: not a in B ; :: thesis: ex S being Formula-finset st
( [S,a] in R & ( for b being object st b in S holds
B,R |- b ) )
consider P being Formula-sequence such that
A3: a in rng P and
A4: P is B,R -correct by A1;
consider c being object such that
A5: c in dom P and
A6: P . c = a by A3, FUNCT_1:def 3;
c in Seg (len P) by A5, FINSEQ_1:def 3;
then reconsider n = c as Nat ;
P,n is_a_correct_step_wrt B,R by A4, A5;
then consider Q being Formula-finset such that
A10: [Q,(P . n)] in R and
A11: for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t ) by A2, A6;
take Q ; :: thesis: ( [Q,a] in R & ( for b being object st b in Q holds
B,R |- b ) )
thus [Q,a] in R by A6, A10; :: thesis: for b being object st b in Q holds
B,R |- b
let u be object ; :: thesis: ( u in Q implies B,R |- u )
assume u in Q ; :: thesis: B,R |- u
then consider k being Nat such that
A15: k in dom P and
k < n and
A17: P . k = u by A11;
u in rng P by A15, A17, FUNCT_1:3;
hence B,R |- u by A4; :: thesis: verum