let X be set ; :: thesis: for C being countable Language
for phi being wff string of C st X c= AllFormulasOf C & phi is X -implied holds
phi is X -provable
let C be countable Language; :: thesis: for phi being wff string of C st X c= AllFormulasOf C & phi is X -implied holds
phi is X -provable
let phi be wff string of C; :: thesis: ( X c= AllFormulasOf C & phi is X -implied implies phi is X -provable )
reconsider S = C as Language ;
reconsider DD = {(R9 S)} as RuleSet of S ;
set FF = AllFormulasOf C;
set D = C -rules ;
assume X c= AllFormulasOf C ; :: thesis: ( not phi is X -implied or phi is X -provable )
then reconsider Y = X as Subset of (AllFormulasOf C) ;
assume phi is X -implied ; :: thesis: phi is X -provable
then reconsider phii = phi as wff X -implied string of C ;
set psi = xnot (xnot phii);
xnot (xnot phii) is Y,C -rules -provable by Lm55;
then consider H being set , m being Nat such that
B0: ( H c= Y & [H,(xnot (xnot phii))] is m, {} ,C -rules -derivable ) by DefProvable3;
reconsider seqt = [H,(xnot (xnot phii))] as C -sequent-like set by B0;
BB1: (seqt `1) \+\ H = {} ;
reconsider HH = H as S -premises-like set by BB1, FOMODEL0:29;
reconsider HC = H as C -premises-like set by BB1, FOMODEL0:29;
reconsider a = phi as wff string of S ;
[HC,phi] null 1 is 1,{[HC,(xnot (xnot phi))]},{(R9 C)} -derivable ;
then [HC,phi] is m + 1, {} ,(C -rules) \/ {(R9 C)} -derivable by Lm28, B0;
then phi is Y,(C -rules) \/ {(R9 C)} -provable by B0, DefProvable3;
hence phi is X -provable by DefProvable4; :: thesis: verum