let X be Subset of MC-wff ; :: thesis:
let p, q, r be Element of MC-wff ; :: thesis:
thus p => (q => p) in CnS4 X :: thesis:

A1: p => (q => p) in CnIPC X by Th1;
CnIPC X c= CnS4 X by Th81;
hence p => (q => p) in CnS4 X by A1; :: thesis:

end;

thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X :: thesis:

A2: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2;
CnIPC X c= CnS4 X by Th81;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X by A2; :: thesis:

end;

thus (p '&' q) => p in CnS4 X :: thesis:

A3: (p '&' q) => p in CnIPC X by Th3;
CnIPC X c= CnS4 X by Th81;
hence (p '&' q) => p in CnS4 X by A3; :: thesis:

end;

thus (p '&' q) => q in CnS4 X :: thesis:

A4: (p '&' q) => q in CnIPC X by Th4;
CnIPC X c= CnS4 X by Th81;
hence (p '&' q) => q in CnS4 X by A4; :: thesis:

end;

thus p => (q => (p '&' q)) in CnS4 X :: thesis:

A5: p => (q => (p '&' q)) in CnIPC X by Th5;
CnIPC X c= CnS4 X by Th81;
hence p => (q => (p '&' q)) in CnS4 X by A5; :: thesis:

end;

thus p => (p 'or' q) in CnS4 X :: thesis:

A6: p => (p 'or' q) in CnIPC X by Th6;
CnIPC X c= CnS4 X by Th81;
hence p => (p 'or' q) in CnS4 X by A6; :: thesis:

end;

thus q => (p 'or' q) in CnS4 X :: thesis:

A7: q => (p 'or' q) in CnIPC X by Th7;
CnIPC X c= CnS4 X by Th81;
hence q => (p 'or' q) in CnS4 X by A7; :: thesis:

end;

thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X :: thesis:

A8: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8;
CnIPC X c= CnS4 X by Th81;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X by A8; :: thesis:

end;

thus FALSUM => p in CnS4 X :: thesis:

A9: FALSUM => p in CnIPC X by Th9;
CnIPC X c= CnS4 X by Th81;
hence FALSUM => p in CnS4 X by A9; :: thesis:

end;

thus p 'or' (p => FALSUM ) in CnS4 X :: thesis:

for T being Subset of MC-wff st T is S4_theory & X c= T holds
p 'or' (p => FALSUM ) in T by Def22;
hence p 'or' (p => FALSUM ) in CnS4 X by Def23; :: thesis:

end;