set FF = AllFormulasOf S;
set Q = S -sequents ;
defpred S1[] means ex H being set ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable );
{} /\ S is S -sequents-like
;
then reconsider e = {} as Element of bool (S -sequents) ;
thus
( x is X,D -provable implies S1[] )
( ex H being set ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable ) implies x is X,D -provable )proof
assume
x is
X,
D -provable
;
S1[]
then consider seqt being
object such that A1:
(
seqt `1 c= X &
seqt `2 = x &
{seqt} is
D -derivable )
;
A2:
(
seqt `1 c= X &
seqt `2 = x &
{seqt} is
{} ,
D -derivable )
by A1;
then
(
{seqt} c= S -sequents &
seqt in {seqt} )
by TARSKI:def 1, Def3;
then
seqt in S -sequents
;
then consider premises being
Subset of
(AllFormulasOf S),
conclusion being
wff string of
S such that A3:
(
seqt = [premises,conclusion] &
premises is
finite )
;
consider mm being
Element of
NAT such that A4:
seqt is
mm,
e,
D -derivable
by A2, Lm8;
take H =
seqt `1 ;
ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable )
take m =
mm;
( H c= X & [H,x] is m, {} ,D -derivable )
thus
(
H c= X &
[H,x] is
m,
{} ,
D -derivable )
by A1, A4, A3;
verum
end;
assume
S1[]
; x is X,D -provable
then consider H being set , m being Nat such that
A5:
( H c= X & [H,x] is m, {} ,D -derivable )
;
hence
x is X,D -provable
; verum