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 & R1 S in D & R8 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 & R1 S in D & R8 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 & R1 S in D & R8 S in D holds
xnot phi is X,D -provable
let D be RuleSet of S; :: thesis: ( X is D -inconsistent & D is isotone & R1 S in D & R8 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 R1 S in D or not R8 S in D or xnot phi is X,D -provable )
then consider phi1, phi2 being wff string of S such that
B0: ( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) by DefInc;
reconsider psi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 as wff string of S ;
consider H being set , m being Nat such that
B1: ( H c= X & [H,phi1] is m, {} ,D -derivable ) by B0, DefProvable3;
consider K being set , n being Nat such that
B2: ( K c= X & [K,psi] is n, {} ,D -derivable ) by B0, DefProvable3;
reconsider HHH = H, KKK = K as Subset of X by B1, B2;
reconsider sq1 = [H,phi1], sq2 = [K,psi] as S -sequent-like set by B1, B2;
( 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 B3: ( D is isotone & R1 S in D & R8 S in D ) ; :: thesis: xnot phi is X,D -provable
then reconsider DD = D as non empty isotone RuleSet of S ;
reconsider E1 = R1 S, E8 = R8 S as Element of DD by B3;
B4: ( DD \/ {E1} = DD null E1 & DD \/ {E8} = DD null E8 & D \/ D is isotone & (D \/ D) \/ {(R8 S)} is isotone & not D is empty & HHH \/ KKK c= X ) by B3;
B7: ( [((J \/ J) null (n + 1)),phi1] is n + 1,{[J,phi1]},{(R1 S)} -derivable & [((J \/ J) null (m + 1)),psi] is m + 1,{[J,psi]},{(R1 S)} -derivable ) ;
[(HH \/ (KK \/ {phi})),phi1] is m + 1, {} ,D \/ {(R1 S)} -derivable by Lm28, B1, B3;
then [J,phi1] is m + 1, {} ,D -derivable by B4, XBOOLE_1:4;
then BB5: [J,phi1] is (m + 1) + (n + 1), {} ,D -derivable by B7, B4, Lm28;
[(KK \/ (HH \/ {phi})),psi] is n + 1, {} ,D \/ {(R1 S)} -derivable by Lm28, B2, B3;
then [J,psi] is n + 1, {} ,D -derivable by B4, XBOOLE_1:4;
then BB6: [J,psi] is (n + 1) + (m + 1), {} ,D -derivable by B7, Lm28, B4;
[((KK \/ HH) null (phi1 ^ phi2)),(xnot phi)] is 1,{[J,phi1],[J,psi]},{(R8 S)} -derivable ;
then [(KK \/ HH),(xnot phi)] is ((m + n) + 2) + 1,({} null S) \/ ({} null S),(D \/ D) \/ {(R8 S)} -derivable by Lm40, BB5, BB6, B3;
hence xnot phi is X,D -provable by B4, DefProvable3; :: thesis: verum