let X be set ; :: thesis: for S being Language
for D being RuleSet of S holds
( X is D -consistent iff for Y being finite Subset of X holds Y is D -consistent )
let S be Language; :: thesis: for D being RuleSet of S holds
( X is D -consistent iff for Y being finite Subset of X holds Y is D -consistent )
let D be RuleSet of S; :: thesis: ( X is D -consistent iff for Y being finite Subset of X holds Y is D -consistent )
set N = TheNorSymbOf S;
thus ( X is D -consistent implies for Y being finite Subset of X holds Y is D -consistent ) ; :: thesis: ( ( for Y being finite Subset of X holds Y is D -consistent ) implies X is D -consistent )
assume A1: for Y being finite Subset of X holds Y is D -consistent ; :: thesis: X is D -consistent
given phi1, phi2 being wff string of S such that A2: ( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) ; :: according to FOMODEL4:def 15 :: thesis: contradiction
reconsider phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 as non 0wff wff non exal string of S ;
consider H1 being set , m1 being Nat such that
A3: ( H1 c= X & [H1,phi1] is m1, {} ,D -derivable ) by A2;
consider H2 being set , m2 being Nat such that
A4: ( H2 c= X & [H2,phi] is m2, {} ,D -derivable ) by A2;
reconsider seqt1 = [H1,phi1], seqt2 = [H2,phi] as S -sequent-like object by A3, A4;
( (seqt1 `1) \+\ H1 = {} & (seqt2 `1) \+\ H2 = {} ) ;
then reconsider H11 = H1, H22 = H2 as S -premises-like Subset of X by A3, A4;
A5: phi1 is H1 null H2,D -provable by A3;
phi is H2 null H1,D -provable by A4;
then H11 \/ H22 is D -inconsistent by A5;
hence contradiction by A1; :: thesis: verum