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 = {(R#9 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 Lm77;
then consider H being set , m being Nat such that
A1: ( H c= Y & [H,(xnot (xnot phii))] is m, {} ,C -rules -derivable ) ;
reconsider seqt = [H,(xnot (xnot phii))] as C -sequent-like object by A1;
A2: (seqt `1) \+\ H = {} ;
reconsider HH = H as S -premises-like set by A2;
reconsider HC = H as C -premises-like set by A2;
reconsider a = phi as wff string of S ;
[HC,phi] null 1 is 1,{[HC,(xnot (xnot phi))]},{(R#9 C)} -derivable ;
then [HC,phi] is m + 1, {} ,(C -rules) \/ {(R#9 C)} -derivable by Lm22, A1;
then phi is Y,(C -rules) \/ {(R#9 C)} -provable by A1;
hence phi is X -provable ; :: thesis: verum