let A be non empty Subset of GRZ-formula-set; 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; 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; ( 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
; 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
; ( [Q,t] in R & A,R |- Q )
thus
[Q,t] in R
by A6, A10; A,R |- Q
let u be GRZ-formula; GRZLOG_1:def 33 ( u in Q implies A,R |- u )
assume
u in Q
; 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; verum