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