let X be set ; :: thesis: for S being Language
for D being RuleSet of S holds
( not X is D -inconsistent iff for Y being finite Subset of X holds not Y is D -inconsistent )
let S be Language; :: thesis: for D being RuleSet of S holds
( not X is D -inconsistent iff for Y being finite Subset of X holds not Y is D -inconsistent )
let D be RuleSet of S; :: thesis: ( not X is D -inconsistent iff for Y being finite Subset of X holds not Y is D -inconsistent )
set N = TheNorSymbOf S;
thus ( not X is D -inconsistent implies for Y being finite Subset of X holds not Y is D -inconsistent ) by Th16; :: thesis: ( ( for Y being finite Subset of X holds not Y is D -inconsistent ) implies not X is D -inconsistent )
assume C4: for Y being finite Subset of X holds not Y is D -inconsistent ; :: thesis: not X is D -inconsistent
assume X is D -inconsistent ; :: thesis: contradiction
then consider phi1, phi2 being wff string of S such that
C0: ( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) by DefInc;
reconsider phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 as non 0wff wff non exal string of S ;
consider H1 being set , m1 being Nat such that
C1: ( H1 c= X & [H1,phi1] is m1, {} ,D -derivable ) by DefProvable3, C0;
consider H2 being set , m2 being Nat such that
C2: ( H2 c= X & [H2,phi] is m2, {} ,D -derivable ) by DefProvable3, C0;
reconsider seqt1 = [H1,phi1], seqt2 = [H2,phi] as S -sequent-like set by C1, C2;
( (seqt1 `1) \+\ H1 = {} & (seqt2 `1) \+\ H2 = {} ) ;
then reconsider H11 = H1, H22 = H2 as S -premises-like Subset of X by C1, C2, FOMODEL0:29;
CC3: phi1 is H1 null H2,D -provable by C1, DefProvable3;
phi is H2 null H1,D -provable by C2, DefProvable3;
then H11 \/ H22 is D -inconsistent by CC3, DefInc;
hence contradiction by C4; :: thesis: verum