let X be Subset of MC-wff; :: thesis: for p, q, r being Element of MC-wff holds
( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
let p, q, r be Element of MC-wff ; :: thesis: ( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A1: CnIPC X c= CnS4 X by Th81;
p => (q => p) in CnIPC X by Th1;
hence p => (q => p) in CnS4 X by A1; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A2: CnIPC X c= CnS4 X by Th81;
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X by A2; :: thesis: ( (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A3: CnIPC X c= CnS4 X by Th81;
(p '&' q) => p in CnIPC X by Th3;
hence (p '&' q) => p in CnS4 X by A3; :: thesis: ( (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A4: CnIPC X c= CnS4 X by Th81;
(p '&' q) => q in CnIPC X by Th4;
hence (p '&' q) => q in CnS4 X by A4; :: thesis: ( p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A5: CnIPC X c= CnS4 X by Th81;
p => (q => (p '&' q)) in CnIPC X by Th5;
hence p => (q => (p '&' q)) in CnS4 X by A5; :: thesis: ( p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A6: CnIPC X c= CnS4 X by Th81;
p => (p 'or' q) in CnIPC X by Th6;
hence p => (p 'or' q) in CnS4 X by A6; :: thesis: ( q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A7: CnIPC X c= CnS4 X by Th81;
q => (p 'or' q) in CnIPC X by Th7;
hence q => (p 'or' q) in CnS4 X by A7; :: thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A8: CnIPC X c= CnS4 X by Th81;
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X by A8; :: thesis: ( FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A9: CnIPC X c= CnS4 X by Th81;
FALSUM => p in CnIPC X by Th9;
hence FALSUM => p in CnS4 X by A9; :: thesis: p 'or' (p => FALSUM) in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
p 'or' (p => FALSUM) in T ;
hence p 'or' (p => FALSUM) in CnS4 X by Def23; :: thesis: verum