let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for t being GRZ-formula holds
( not A,R |- t or t in A or ex S being GRZ-formula-finset st
( [S,t] in R & A,R |- S ) )
let R be GRZ-rule; :: thesis: for t being GRZ-formula holds
( not A,R |- t or t in A or ex S being GRZ-formula-finset st
( [S,t] in R & A,R |- S ) )
let t be GRZ-formula; :: thesis: ( not A,R |- t or t in A or ex S being GRZ-formula-finset st
( [S,t] in R & A,R |- S ) )
assume that
A1: A,R |- t and
A2: not t in A ; :: thesis: ex S being GRZ-formula-finset st
( [S,t] in R & A,R |- S )
consider P being GRZ-formula-sequence such that
A3: t in rng P and
A4: P is A,R -correct by A1;
consider a being object such that
A5: a in dom P and
A6: P . a = t by A3, FUNCT_1:def 3;
reconsider n = a as Element of NAT by A5;
P,n is_a_correct_step_wrt A,R by A4, A5;
then consider Q being GRZ-formula-finset such that
A10: [Q,(P . n)] in R and
A11: for q being FinSequence st q in Q holds
ex k being Element of NAT st
( k in dom P & k < n & P . k = q ) by A2, A6;
take Q ; :: thesis: ( [Q,t] in R & A,R |- Q )
thus [Q,t] in R by A6, A10; :: thesis: A,R |- Q
let u be GRZ-formula; :: according to GRZLOG_1:def 33 :: thesis: ( u in Q implies A,R |- u )
assume u in Q ; :: thesis: A,R |- u
then consider k being Element of 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 A,R |- u by A4; :: thesis: verum