let X be set ; :: thesis: for S being Language
for phi being wff string of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & X \/ {phi} is D -inconsistent holds
xnot phi is X,D -provable
let S be Language; :: thesis: for phi being wff string of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & X \/ {phi} is D -inconsistent holds
xnot phi is X,D -provable
let phi be wff string of S; :: thesis: for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & X \/ {phi} is D -inconsistent holds
xnot phi is X,D -provable
let D be RuleSet of S; :: thesis: ( D is isotone & R1 S in D & R8 S in D & X \/ {phi} is D -inconsistent implies xnot phi is X,D -provable )
set XX = X \/ {phi};
set N = TheNorSymbOf S;
set G1 = R1 S;
set G8 = R8 S;
set E1 = {(R1 S)};
set E8 = {(R8 S)};
assume B10: ( D is isotone & R1 S in D & R8 S in D ) ; :: thesis: ( not X \/ {phi} is D -inconsistent or xnot phi is X,D -provable )
then reconsider F1 = {(R1 S)}, F8 = {(R8 S)} as Subset of D by ZFMISC_1:31;
assume X \/ {phi} is D -inconsistent ; :: thesis: xnot phi is X,D -provable
then consider phi1, phi2 being wff string of S such that
B0: ( phi1 is X \/ {phi},D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X \/ {phi},D -provable ) by DefInc;
set nphi1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
consider H1 being set , m1 being Nat such that
B1: ( H1 c= X \/ {phi} & [H1,phi1] is m1, {} ,D -derivable ) by DefProvable3, B0;
consider H2 being set , m2 being Nat such that
B2: ( H2 c= X \/ {phi} & [H2,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is m2, {} ,D -derivable ) by DefProvable3, B0;
reconsider seqt1 = [H1,phi1], seqt2 = [H2,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] as S -sequent-like set by B1, B2;
( (seqt1 `1) \+\ H1 = {} & (seqt2 `1) \+\ H2 = {} ) ;
then reconsider H11 = H1, H22 = H2 as S -premises-like Subset of (X \/ {phi}) by B1, B2, FOMODEL0:29;
reconsider H111 = H11 \ {phi}, H222 = H22 \ {phi} as S -premises-like Subset of X by XBOOLE_1:43;
( H11 \ H111 = H11 /\ {phi} & H22 \ H222 = H22 /\ {phi} ) by XBOOLE_1:48;
then reconsider pH1 = H11 \ H111, pH2 = H22 \ H222 as S -premises-like Subset of {phi} ;
reconsider H = H11 \/ H22 as S -premises-like Subset of (X \/ {phi}) ;
reconsider h = H \ {phi} as S -premises-like Subset of X by XBOOLE_1:43;
reconsider hp = H /\ {phi} as S -premises-like Subset of {phi} ;
reconsider Phi = {phi} as S -premises-like set ;
set M = (m1 + m2) + 1;
reconsider hh = h \/ {phi} as S -premises-like set ;
reconsider e = {} null S as S -sequents-like set ;
set x = [hh,phi1];
set y = [hh,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)];
[((H11 \/ (H22 \/ Phi)) null (m2 + 1)),phi1] is m2 + 1,{[H11,phi1]},{(R1 S)} -derivable ;
then [(H11 \/ (H22 \/ {phi})),phi1] is m1 + (m2 + 1), {} ,D \/ {(R1 S)} -derivable by B1, Lm28, B10;
then [(H \/ {phi}),phi1] is (m1 + m2) + 1, {} ,D null F1 -derivable by XBOOLE_1:4;
then [((h \/ hp) \/ {phi}),phi1] is (m1 + m2) + 1, {} ,D -derivable by FOMODEL0:48;
then BB3: [(h \/ ({phi} null hp)),phi1] is (m1 + m2) + 1, {} ,D -derivable by XBOOLE_1:4;
[((H22 \/ (H11 \/ {phi})) null (m1 + 1)),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is m1 + 1,{[H22,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R1 S)} -derivable ;
then [(H22 \/ (H11 \/ {phi})),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is m2 + (m1 + 1), {} ,D \/ {(R1 S)} -derivable by B2, Lm28, B10;
then [(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is (m1 + m2) + 1, {} ,D null F1 -derivable by XBOOLE_1:4;
then [((h \/ hp) \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is (m1 + m2) + 1, {} ,D -derivable by FOMODEL0:48;
then BB4: [(h \/ ({phi} null hp)),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] is (m1 + m2) + 1, {} ,D -derivable by XBOOLE_1:4;
[(h null (phi1 ^ phi2)),(xnot phi)] is 1,{[(h \/ {phi}),phi1],[(h \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R8 S)} -derivable ;
then [h,(xnot phi)] is ((m1 + m2) + 1) + 1,e \/ e,(D \/ D) \/ {(R8 S)} -derivable by BB3, BB4, Lm40, B10;
then [h,(xnot phi)] is ((m1 + m2) + 1) + 1, {} ,D null F8 -derivable ;
hence xnot phi is X,D -provable by DefProvable3; :: thesis: verum