let X be set ; :: thesis: for S being Language
for phi being wff string of S
for D being RuleSet of S st X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D 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 X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D holds
xnot phi is X,D -provable
let phi be wff string of S; :: thesis: for D being RuleSet of S st X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D holds
xnot phi is X,D -provable
let D be RuleSet of S; :: thesis: ( X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D implies xnot phi is X,D -provable )
set N = TheNorSymbOf S;
assume X is D -inconsistent ; :: thesis: ( not D is isotone or not R#1 S in D or not R#8 S in D or xnot phi is X,D -provable )
then consider phi1, phi2 being wff string of S such that
A1: ( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) by Def65;
reconsider psi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 as wff string of S ;
consider H being set , m being Nat such that
A2: ( H c= X & [H,phi1] is m, {} ,D -derivable ) by A1, Def62;
consider K being set , n being Nat such that
A3: ( K c= X & [K,psi] is n, {} ,D -derivable ) by A1, Def62;
reconsider HHH = H, KKK = K as Subset of X by A2, A3;
reconsider sq1 = [H,phi1], sq2 = [K,psi] as S -sequent-like set by A2, A3;
( H = sq1 `1 & K = sq2 `1 ) by MCART_1:7;
then reconsider HH = H, KK = K as S -premises-like set ;
reconsider J = (HH \/ KK) \/ {phi} as S -premises-like set ;
assume A4: ( D is isotone & R#1 S in D & R#8 S in D ) ; :: thesis: xnot phi is X,D -provable
then reconsider DD = D as non empty isotone RuleSet of S ;
reconsider E1 = R#1 S, E8 = R#8 S as Element of DD by A4;
A5: ( DD \/ {E1} = DD null E1 & DD \/ {E8} = DD null E8 & D \/ D is isotone & (D \/ D) \/ {(R#8 S)} is isotone & not D is empty & HHH \/ KKK c= X ) by A4;
A6: ( [((J \/ J) null (n + 1)),phi1] is n + 1,{[J,phi1]},{(R#1 S)} -derivable & [((J \/ J) null (m + 1)),psi] is m + 1,{[J,psi]},{(R#1 S)} -derivable ) ;
[(HH \/ (KK \/ {phi})),phi1] is m + 1, {} ,D \/ {(R#1 S)} -derivable by Lm21, A2, A4;
then [J,phi1] is m + 1, {} ,D -derivable by A5, XBOOLE_1:4;
then A7: [J,phi1] is (m + 1) + (n + 1), {} ,D -derivable by A6, A5, Lm21;
[(KK \/ (HH \/ {phi})),psi] is n + 1, {} ,D \/ {(R#1 S)} -derivable by Lm21, A3, A4;
then [J,psi] is n + 1, {} ,D -derivable by A5, XBOOLE_1:4;
then A8: [J,psi] is (n + 1) + (m + 1), {} ,D -derivable by A6, Lm21, A5;
[((KK \/ HH) null (phi1 ^ phi2)),(xnot phi)] is 1,{[J,phi1],[J,psi]},{(R#8 S)} -derivable ;
then [(KK \/ HH),(xnot phi)] is ((m + n) + 2) + 1,({} null S) \/ ({} null S),(D \/ D) \/ {(R#8 S)} -derivable by Lm48, A7, A8, A4;
hence xnot phi is X,D -provable by A5, Def62; :: thesis: verum