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[] ) :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable )
take m = mm; :: thesis: ( H c= X & [H,x] is m, {} ,D -derivable )
thus ( H c= X & [H,x] is m, {} ,D -derivable ) by A1, A4, A3; :: thesis: verum
end;
assume S1[] ; :: thesis: 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 ) ;
now :: thesis: ex seqt being object st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable )
take seqt = [H,x]; :: thesis: ( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable )
( seqt `1 c= X & seqt `2 = x & {seqt} is {} ,D -derivable ) by A5, Lm12;
hence ( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) ; :: thesis: verum
end;
hence x is X,D -provable ; :: thesis: verum