:: INTPRO_1 semantic presentation

begin

definition
let E be set ;
attrE is with_FALSUM  means :Def1: :: INTPRO_1:def 1
<*0*> in E;
end;

:: deftheorem Def1 defines with_FALSUM INTPRO_1:def_1_:_
 for E being set holds
( E is with_FALSUM iff <*0*> in E );

definition
let E be set ;
attrE is with_int_implication  means :Def2: :: INTPRO_1:def 2
 for p, q being FinSequence st p in E & q in E holds
(<*1*> ^ p) ^ q in E;
end;

:: deftheorem Def2 defines with_int_implication INTPRO_1:def_2_:_
 for E being set holds
( E is with_int_implication iff for p, q being FinSequence st p in E & q in E holds
(<*1*> ^ p) ^ q in E );

definition
let E be set ;
attrE is with_int_conjunction  means :Def3: :: INTPRO_1:def 3
 for p, q being FinSequence st p in E & q in E holds
(<*2*> ^ p) ^ q in E;
end;

:: deftheorem Def3 defines with_int_conjunction INTPRO_1:def_3_:_
 for E being set holds
( E is with_int_conjunction iff for p, q being FinSequence st p in E & q in E holds
(<*2*> ^ p) ^ q in E );

definition
let E be set ;
attrE is with_int_disjunction  means :Def4: :: INTPRO_1:def 4
 for p, q being FinSequence st p in E & q in E holds
(<*3*> ^ p) ^ q in E;
end;

:: deftheorem Def4 defines with_int_disjunction INTPRO_1:def_4_:_
 for E being set holds
( E is with_int_disjunction iff for p, q being FinSequence st p in E & q in E holds
(<*3*> ^ p) ^ q in E );

definition
let E be set ;
attrE is with_int_propositional_variables  means :Def5: :: INTPRO_1:def 5
 for n being Element of NAT holds <*(5 + (2 * n))*> in E;
end;

:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def_5_:_
 for E being set holds
( E is with_int_propositional_variables iff for n being Element of NAT holds <*(5 + (2 * n))*> in E );

definition
let E be set ;
attrE is with_modal_operator  means :Def6: :: INTPRO_1:def 6
 for p being FinSequence st p in E holds
<*6*> ^ p in E;
end;

:: deftheorem Def6 defines with_modal_operator INTPRO_1:def_6_:_
 for E being set holds
( E is with_modal_operator iff for p being FinSequence st p in E holds
<*6*> ^ p in E );

definition
let E be set ;
attrE is MC-closed  means :Def7: :: INTPRO_1:def 7
( E c= NAT * & E is with_FALSUM & E is with_int_implication & E is with_int_conjunction & E is with_int_disjunction & E is with_int_propositional_variables & E is with_modal_operator );
end;

:: deftheorem Def7 defines MC-closed INTPRO_1:def_7_:_
 for E being set holds
( E is MC-closed iff ( E c= NAT * & E is with_FALSUM & E is with_int_implication & E is with_int_conjunction & E is with_int_disjunction & E is with_int_propositional_variables & E is with_modal_operator ) );

Lm1:  for E being set st E is MC-closed holds
not E is empty
proof
let E be set ; ::_thesis: ( E is MC-closed implies not E is empty )
assume  E is MC-closed ; ::_thesis: not E is empty
then  E is with_FALSUM by Def7;
hence  not E is empty by Def1; ::_thesis: verum
end;

registration
cluster MC-closed  ->  non empty with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator for set ;
coherence
 for b1 being set st b1 is MC-closed holds
( b1 is with_FALSUM & b1 is with_int_implication & b1 is with_int_conjunction & b1 is with_int_disjunction & b1 is with_int_propositional_variables & b1 is with_modal_operator & not b1 is empty ) by Def7, Lm1;
cluster with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator  ->  MC-closed for Element of K6((NAT *));
coherence
 for b1 being Subset of (NAT *) st b1 is with_FALSUM & b1 is with_int_implication & b1 is with_int_conjunction & b1 is with_int_disjunction & b1 is with_int_propositional_variables & b1 is with_modal_operator holds
b1 is MC-closed by Def7;
end;

definition
func MC-wff  ->  set  means :Def8: :: INTPRO_1:def 8
( it is MC-closed & ( for E being set st E is MC-closed holds
it c= E ) );
existence
 ex b1 being set st
( b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) )
proof
A1: <*0*> in NAT * by FINSEQ_1:def_11;
defpred S1[ set ] means  for E being set st E is MC-closed holds
$1 in E;
consider E0 being set  such that
A2: for x being set holds
( x in E0 iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for E being set st E is MC-closed holds
<*0*> in E by Def1;
then reconsider E0 = E0 as non empty set by A2, A1;
take  E0 ; ::_thesis: ( E0 is MC-closed & ( for E being set st E is MC-closed holds
E0 c= E ) )
A4: E0 c= NAT *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E0 or x in NAT * )
thus  ( not x in E0 or x in NAT * ) by A2; ::_thesis: verum
end;
 for p being FinSequence st p in E0 holds
<*6*> ^ p in E0
proof
let p be FinSequence; ::_thesis: ( p in E0 implies <*6*> ^ p in E0 )
assume A5: p in E0 ; ::_thesis: <*6*> ^ p in E0
 p in NAT * by A2, A5;
then reconsider p9 = p as FinSequence of NAT by FINSEQ_1:def_11;
A6: for E being set st E is MC-closed holds
<*6*> ^ p in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies <*6*> ^ p in E )
assume A7: E is MC-closed ; ::_thesis: <*6*> ^ p in E
then  p in E by A2, A5;
hence  <*6*> ^ p in E by A7, Def6; ::_thesis: verum
end;
 <*6*> ^ p9 in NAT * by FINSEQ_1:def_11;
hence  <*6*> ^ p in E0 by A2, A6; ::_thesis: verum
end;
then A8: E0 is with_modal_operator by Def6;
 for n being Element of NAT holds <*(5 + (2 * n))*> in E0
proof
let n be Element of NAT ; ::_thesis: <*(5 + (2 * n))*> in E0
set p = 5 + (2 * n);
reconsider h = <*(5 + (2 * n))*> as FinSequence of NAT ;
A9: h in NAT * by FINSEQ_1:def_11;
 for E being set st E is MC-closed holds
<*(5 + (2 * n))*> in E by Def5;
hence  <*(5 + (2 * n))*> in E0 by A2, A9; ::_thesis: verum
end;
then A10: E0 is with_int_propositional_variables by Def5;
 for p, q being FinSequence st p in E0 & q in E0 holds
(<*3*> ^ p) ^ q in E0
proof
let p, q be FinSequence; ::_thesis: ( p in E0 & q in E0 implies (<*3*> ^ p) ^ q in E0 )
assume that
A11: p in E0 and
A12: q in E0 ; ::_thesis: (<*3*> ^ p) ^ q in E0
A13: q in NAT * by A2, A12;
A14: for E being set st E is MC-closed holds
(<*3*> ^ p) ^ q in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies (<*3*> ^ p) ^ q in E )
assume A15: E is MC-closed ; ::_thesis: (<*3*> ^ p) ^ q in E
then A16: q in E by A2, A12;
 p in E by A2, A11, A15;
hence  (<*3*> ^ p) ^ q in E by A15, A16, Def4; ::_thesis: verum
end;
 p in NAT * by A2, A11;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A13, FINSEQ_1:def_11;
 (<*3*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence  (<*3*> ^ p) ^ q in E0 by A2, A14; ::_thesis: verum
end;
then A17: E0 is with_int_disjunction by Def4;
 for p, q being FinSequence st p in E0 & q in E0 holds
(<*2*> ^ p) ^ q in E0
proof
let p, q be FinSequence; ::_thesis: ( p in E0 & q in E0 implies (<*2*> ^ p) ^ q in E0 )
assume that
A18: p in E0 and
A19: q in E0 ; ::_thesis: (<*2*> ^ p) ^ q in E0
A20: q in NAT * by A2, A19;
A21: for E being set st E is MC-closed holds
(<*2*> ^ p) ^ q in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies (<*2*> ^ p) ^ q in E )
assume A22: E is MC-closed ; ::_thesis: (<*2*> ^ p) ^ q in E
then A23: q in E by A2, A19;
 p in E by A2, A18, A22;
hence  (<*2*> ^ p) ^ q in E by A22, A23, Def3; ::_thesis: verum
end;
 p in NAT * by A2, A18;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A20, FINSEQ_1:def_11;
 (<*2*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence  (<*2*> ^ p) ^ q in E0 by A2, A21; ::_thesis: verum
end;
then A24: E0 is with_int_conjunction by Def3;
 for p, q being FinSequence st p in E0 & q in E0 holds
(<*1*> ^ p) ^ q in E0
proof
let p, q be FinSequence; ::_thesis: ( p in E0 & q in E0 implies (<*1*> ^ p) ^ q in E0 )
assume that
A25: p in E0 and
A26: q in E0 ; ::_thesis: (<*1*> ^ p) ^ q in E0
A27: q in NAT * by A2, A26;
A28: for E being set st E is MC-closed holds
(<*1*> ^ p) ^ q in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies (<*1*> ^ p) ^ q in E )
assume A29: E is MC-closed ; ::_thesis: (<*1*> ^ p) ^ q in E
then A30: q in E by A2, A26;
 p in E by A2, A25, A29;
hence  (<*1*> ^ p) ^ q in E by A29, A30, Def2; ::_thesis: verum
end;
 p in NAT * by A2, A25;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A27, FINSEQ_1:def_11;
 (<*1*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence  (<*1*> ^ p) ^ q in E0 by A2, A28; ::_thesis: verum
end;
then A31: E0 is with_int_implication by Def2;
 <*0*> in E0 by A2, A1, A3;
then  E0 is with_FALSUM by Def1;
hence  E0 is MC-closed by A4, A10, A31, A24, A17, A8; ::_thesis: for E being set st E is MC-closed holds
E0 c= E
let E be set ; ::_thesis: ( E is MC-closed implies E0 c= E )
assume A32: E is MC-closed ; ::_thesis: E0 c= E
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E0 or x in E )
assume  x in E0 ; ::_thesis: x in E
hence  x in E by A2, A32; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) & b2 is MC-closed & ( for E being set st E is MC-closed holds
b2 c= E ) holds
b1 = b2
proof
let E1, E2 be set ; ::_thesis: ( E1 is MC-closed & ( for E being set st E is MC-closed holds
E1 c= E ) & E2 is MC-closed & ( for E being set st E is MC-closed holds
E2 c= E ) implies E1 = E2 )
assume that
A33: E1 is MC-closed and
A34: for E being set st E is MC-closed holds
E1 c= E and
A35: E2 is MC-closed and
A36: for E being set st E is MC-closed holds
E2 c= E ; ::_thesis: E1 = E2
A37: E2 c= E1 by A33, A36;
 E1 c= E2 by A34, A35;
hence  E1 = E2 by A37, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines MC-wff INTPRO_1:def_8_:_
 for b1 being set holds
( b1 = MC-wff iff ( b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) ) );

registration
cluster MC-wff  ->  MC-closed ;
coherence
 MC-wff is MC-closed by Def8;
end;

registration
cluster non empty MC-closed for set ;
existence
 ex b1 being set st
( b1 is MC-closed & not b1 is empty )
proof
take  MC-wff ; ::_thesis: ( MC-wff is MC-closed & not MC-wff is empty )
thus  ( MC-wff is MC-closed & not MC-wff is empty ) ; ::_thesis: verum
end;
end;

registration
cluster MC-wff  ->  functional ;
coherence
 MC-wff is functional
proof
 MC-wff c= NAT * by Def7;
hence  MC-wff is functional ; ::_thesis: verum
end;
end;

registration
cluster  ->  FinSequence-like for Element of MC-wff ;
coherence
 for b1 being Element of MC-wff holds b1 is FinSequence-like
proof
let p be Element of MC-wff ; ::_thesis: p is FinSequence-like
 MC-wff c= NAT * by Def7;
hence  p is FinSequence-like ; ::_thesis: verum
end;
end;

definition
mode MC-formula is Element of MC-wff ;
end;

definition
func FALSUM  ->  MC-formula equals :: INTPRO_1:def 9
<*0*>;
correctness
coherence
<*0*> is MC-formula;
by Def1;
let p, q be Element of MC-wff ;
funcp => q ->  MC-formula equals :: INTPRO_1:def 10
(<*1*> ^ p) ^ q;
correctness
coherence
(<*1*> ^ p) ^ q is MC-formula;
by Def2;
funcp '&' q ->  MC-formula equals :: INTPRO_1:def 11
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is MC-formula;
by Def3;
funcp 'or' q ->  MC-formula equals :: INTPRO_1:def 12
(<*3*> ^ p) ^ q;
correctness
coherence
(<*3*> ^ p) ^ q is MC-formula;
by Def4;
end;

:: deftheorem  defines FALSUM INTPRO_1:def_9_:_
 FALSUM = <*0*>;

:: deftheorem  defines => INTPRO_1:def_10_:_
 for p, q being Element of MC-wff holds p => q = (<*1*> ^ p) ^ q;

:: deftheorem  defines '&' INTPRO_1:def_11_:_
 for p, q being Element of MC-wff holds p '&' q = (<*2*> ^ p) ^ q;

:: deftheorem  defines 'or' INTPRO_1:def_12_:_
 for p, q being Element of MC-wff holds p 'or' q = (<*3*> ^ p) ^ q;

definition
let p be Element of MC-wff ;
func Nes p ->  MC-formula equals :: INTPRO_1:def 13
<*6*> ^ p;
correctness
coherence
<*6*> ^ p is MC-formula;
by Def6;
end;

:: deftheorem  defines Nes INTPRO_1:def_13_:_
 for p being Element of MC-wff holds Nes p = <*6*> ^ p;


definition
let T be Subset of MC-wff;
attrT is IPC_theory  means :Def14: :: INTPRO_1:def 14
 for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) );
correctness
;
end;

:: deftheorem Def14 defines IPC_theory INTPRO_1:def_14_:_
 for T being Subset of MC-wff holds
( T is IPC_theory iff for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) );

definition
let X be Subset of MC-wff;
func CnIPC X ->  Subset of MC-wff means :Def15: :: INTPRO_1:def 15
 for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T );
existence
 ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means  for T being Subset of MC-wff st T is IPC_theory & X c= T holds
$1 in T;
consider Y being set  such that
A1: for a being set holds
( a in Y iff ( a in MC-wff & S1[a] ) ) from XBOOLE_0:sch_1();
 Y c= MC-wff
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in MC-wff )
assume  a in Y ; ::_thesis: a in MC-wff
hence  a in MC-wff by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of MC-wff ;
take  Z ; ::_thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T )
thus  for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of MC-wff; ::_thesis: ( ( for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) and
A3: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ; ::_thesis: Y = Z
 for a being set holds
( a in Y iff a in Z )
proof
let a be set ; ::_thesis: ( a in Y iff a in Z )
hereby  ::_thesis: ( a in Z implies a in Y )
assume A4: a in Y ; ::_thesis: a in Z
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
t in T by A2, A4;
hence  a in Z by A3; ::_thesis: verum
end;
assume A5: a in Z ; ::_thesis: a in Y
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
t in T by A3, A5;
hence  a in Y by A2; ::_thesis: verum
end;
hence  Y = Z by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines CnIPC INTPRO_1:def_15_:_
 for X, b2 being Subset of MC-wff holds
( b2 = CnIPC X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) );

definition
func IPC-Taut  ->  Subset of MC-wff equals :: INTPRO_1:def 16
 CnIPC ({} MC-wff);
correctness
coherence
CnIPC ({} MC-wff) is Subset of MC-wff;
;
end;

:: deftheorem  defines IPC-Taut INTPRO_1:def_16_:_
 IPC-Taut = CnIPC ({} MC-wff);

definition
let p be Element of MC-wff ;
func neg p ->  MC-formula equals :: INTPRO_1:def 17
p => FALSUM;
correctness
coherence
p => FALSUM is MC-formula;
;
end;

:: deftheorem  defines neg INTPRO_1:def_17_:_
 for p being Element of MC-wff holds neg p = p => FALSUM;

definition
func IVERUM  ->  MC-formula equals :: INTPRO_1:def 18
FALSUM => FALSUM;
correctness
coherence
FALSUM => FALSUM is MC-formula;
;
end;

:: deftheorem  defines IVERUM INTPRO_1:def_18_:_
 IVERUM = FALSUM => FALSUM;

theorem Th1: :: INTPRO_1:1
for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (q => p) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds p => (q => p) in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: p => (q => p) in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
p => (q => p) in T by Def14;
hence  p => (q => p) in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th2: :: INTPRO_1:2
for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X
let p, q, r be Element of MC-wff ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p => (q => r)) => ((p => q) => (p => r)) in T by Def14;
hence  (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th3: :: INTPRO_1:3
for X being Subset of MC-wff
for p, q being Element of MC-wff holds (p '&' q) => p in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds (p '&' q) => p in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: (p '&' q) => p in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p '&' q) => p in T by Def14;
hence  (p '&' q) => p in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th4: :: INTPRO_1:4
for X being Subset of MC-wff
for p, q being Element of MC-wff holds (p '&' q) => q in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds (p '&' q) => q in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: (p '&' q) => q in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p '&' q) => q in T by Def14;
hence  (p '&' q) => q in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th5: :: INTPRO_1:5
for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (q => (p '&' q)) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds p => (q => (p '&' q)) in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: p => (q => (p '&' q)) in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
p => (q => (p '&' q)) in T by Def14;
hence  p => (q => (p '&' q)) in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th6: :: INTPRO_1:6
for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (p 'or' q) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds p => (p 'or' q) in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: p => (p 'or' q) in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
p => (p 'or' q) in T by Def14;
hence  p => (p 'or' q) in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th7: :: INTPRO_1:7
for X being Subset of MC-wff
for q, p being Element of MC-wff holds q => (p 'or' q) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for q, p being Element of MC-wff holds q => (p 'or' q) in CnIPC X
let q, p be Element of MC-wff ; ::_thesis: q => (p 'or' q) in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
q => (p 'or' q) in T by Def14;
hence  q => (p 'or' q) in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th8: :: INTPRO_1:8
for X being Subset of MC-wff
for p, r, q being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, r, q being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
let p, r, q be Element of MC-wff ; ::_thesis: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p => r) => ((q => r) => ((p 'or' q) => r)) in T by Def14;
hence  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th9: :: INTPRO_1:9
for X being Subset of MC-wff
for p being Element of MC-wff holds FALSUM => p in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff holds FALSUM => p in CnIPC X
let p be Element of MC-wff ; ::_thesis: FALSUM => p in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
FALSUM => p in T by Def14;
hence  FALSUM => p in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th10: :: INTPRO_1:10
for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnIPC X & p => q in CnIPC X holds
q in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff st p in CnIPC X & p => q in CnIPC X holds
q in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X )
assume that
A1: p in CnIPC X and
A2: p => q in CnIPC X ; ::_thesis: q in CnIPC X
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
q in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory & X c= T implies q in T )
assume that
A3: T is IPC_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def15;
 p in T by A1, A3, A4, Def15;
hence  q in T by A3, A5, Def14; ::_thesis: verum
end;
hence  q in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th11: :: INTPRO_1:11
for T, X being Subset of MC-wff st T is IPC_theory & X c= T holds
CnIPC X c= T
proof
let T, X be Subset of MC-wff; ::_thesis: ( T is IPC_theory & X c= T implies CnIPC X c= T )
assume that
A1: T is IPC_theory and
A2: X c= T ; ::_thesis: CnIPC X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC X or a in T )
thus  ( not a in CnIPC X or a in T ) by A1, A2, Def15; ::_thesis: verum
end;

theorem Th12: :: INTPRO_1:12
for X being Subset of MC-wff holds X c= CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: X c= CnIPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnIPC X )
assume A1: a in X ; ::_thesis: a in CnIPC X
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
t in T by A1;
hence  a in CnIPC X by Def15; ::_thesis: verum
end;

theorem Th13: :: INTPRO_1:13
for X, Y being Subset of MC-wff st X c= Y holds
CnIPC X c= CnIPC Y
proof
let X, Y be Subset of MC-wff; ::_thesis: ( X c= Y implies CnIPC X c= CnIPC Y )
assume A1: X c= Y ; ::_thesis: CnIPC X c= CnIPC Y
thus  CnIPC X c= CnIPC Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC X or a in CnIPC Y )
assume A2: a in CnIPC X ; ::_thesis: a in CnIPC Y
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is IPC_theory & Y c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory & Y c= T implies t in T )
assume that
A3: T is IPC_theory and
A4: Y c= T ; ::_thesis: t in T
 X c= T by A1, A4, XBOOLE_1:1;
hence  t in T by A2, A3, Def15; ::_thesis: verum
end;
hence  a in CnIPC Y by Def15; ::_thesis: verum
end;
end;

Lm2:  for X being Subset of MC-wff holds CnIPC (CnIPC X) c= CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC (CnIPC X) c= CnIPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC (CnIPC X) or a in CnIPC X )
assume A1: a in CnIPC (CnIPC X) ; ::_thesis: a in CnIPC X
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is IPC_theory & X c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory & X c= T implies t in T )
assume that
A2: T is IPC_theory and
A3: X c= T ; ::_thesis: t in T
 CnIPC X c= T by A2, A3, Th11;
hence  t in T by A1, A2, Def15; ::_thesis: verum
end;
hence  a in CnIPC X by Def15; ::_thesis: verum
end;

theorem :: INTPRO_1:14
for X being Subset of MC-wff holds CnIPC (CnIPC X) = CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC (CnIPC X) = CnIPC X
A1: CnIPC X c= CnIPC (CnIPC X) by Th12;
 CnIPC (CnIPC X) c= CnIPC X by Lm2;
hence  CnIPC (CnIPC X) = CnIPC X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm3:  for X being Subset of MC-wff holds CnIPC X is IPC_theory
proof
let X be Subset of MC-wff; ::_thesis: CnIPC X is IPC_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def_14 ::_thesis: for q, r being Element of MC-wff holds
( p => (q => p) in CnIPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
let q, r be Element of MC-wff ; ::_thesis: ( p => (q => p) in CnIPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  p => (q => p) in CnIPC X by Th1; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2; ::_thesis: ( (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  (p '&' q) => p in CnIPC X by Th3; ::_thesis: ( (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  (p '&' q) => q in CnIPC X by Th4; ::_thesis: ( p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  p => (q => (p '&' q)) in CnIPC X by Th5; ::_thesis: ( p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  p => (p 'or' q) in CnIPC X by Th6; ::_thesis: ( q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  q => (p 'or' q) in CnIPC X by Th7; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8; ::_thesis: ( FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus  FALSUM => p in CnIPC X by Th9; ::_thesis: ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X )
thus  ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) by Th10; ::_thesis: verum
end;

registration
let X be Subset of MC-wff;
cluster CnIPC X ->  IPC_theory ;
coherence
 CnIPC X is IPC_theory by Lm3;
end;

theorem Th15: :: INTPRO_1:15
for T being Subset of MC-wff holds
( T is IPC_theory iff CnIPC T = T )
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory iff CnIPC T = T )
hereby  ::_thesis: ( CnIPC T = T implies T is IPC_theory )
assume A1: T is IPC_theory ; ::_thesis: CnIPC T = T
A2: CnIPC T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC T or a in T )
assume  a in CnIPC T ; ::_thesis: a in T
hence  a in T by A1, Def15; ::_thesis: verum
end;
 T c= CnIPC T by Th12;
hence  CnIPC T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( CnIPC T = T implies T is IPC_theory ) ; ::_thesis: verum
end;

theorem :: INTPRO_1:16
for T being Subset of MC-wff st T is IPC_theory holds
IPC-Taut c= T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory implies IPC-Taut c= T )
assume A1: T is IPC_theory ; ::_thesis: IPC-Taut c= T
 IPC-Taut c= CnIPC T by Th13, XBOOLE_1:2;
hence  IPC-Taut c= T by A1, Th15; ::_thesis: verum
end;

registration
cluster IPC-Taut  ->  IPC_theory ;
coherence
 IPC-Taut is IPC_theory ;
end;

begin

theorem Th17: :: INTPRO_1:17
for p being Element of MC-wff holds p => p in IPC-Taut
proof
let p be Element of MC-wff ; ::_thesis: p => p in IPC-Taut
A1: p => (p => p) in IPC-Taut by Def14;
A2: p => ((p => p) => p) in IPC-Taut by Def14;
 (p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) in IPC-Taut by Def14;
then  (p => (p => p)) => (p => p) in IPC-Taut by A2, Def14;
hence  p => p in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th18: :: INTPRO_1:18
for q, p being Element of MC-wff st q in IPC-Taut holds
p => q in IPC-Taut
proof
let q, p be Element of MC-wff ; ::_thesis: ( q in IPC-Taut implies p => q in IPC-Taut )
 q => (p => q) in IPC-Taut by Def14;
hence  ( q in IPC-Taut implies p => q in IPC-Taut ) by Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:19
IVERUM in IPC-Taut by Def14;

theorem :: INTPRO_1:20
for p, q being Element of MC-wff holds (p => q) => (p => p) in IPC-Taut by Th17, Th18;

theorem :: INTPRO_1:21
for q, p being Element of MC-wff holds (q => p) => (p => p) in IPC-Taut by Th17, Th18;

theorem Th22: :: INTPRO_1:22
for q, r, p being Element of MC-wff holds (q => r) => ((p => q) => (p => r)) in IPC-Taut
proof
let q, r, p be Element of MC-wff ; ::_thesis: (q => r) => ((p => q) => (p => r)) in IPC-Taut
A1: (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
A2: ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in IPC-Taut by Def14;
 ((p => (q => r)) => ((p => q) => (p => r))) => ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut by Def14;
then  (q => r) => ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by A1, Def14;
then A3: ((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))) in IPC-Taut by A2, Def14;
 (q => r) => (p => (q => r)) in IPC-Taut by Def14;
hence  (q => r) => ((p => q) => (p => r)) in IPC-Taut by A3, Def14; ::_thesis: verum
end;

theorem Th23: :: INTPRO_1:23
for p, q, r being Element of MC-wff st p => (q => r) in IPC-Taut holds
q => (p => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ( p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut )
assume A1: p => (q => r) in IPC-Taut ; ::_thesis: q => (p => r) in IPC-Taut
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in IPC-Taut by Th22;
 (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then  (p => q) => (p => r) in IPC-Taut by A1, Def14;
then A3: (q => (p => q)) => (q => (p => r)) in IPC-Taut by A2, Def14;
 q => (p => q) in IPC-Taut by Def14;
hence  q => (p => r) in IPC-Taut by A3, Def14; ::_thesis: verum
end;

theorem Th24: :: INTPRO_1:24
for p, q, r being Element of MC-wff holds (p => q) => ((q => r) => (p => r)) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: (p => q) => ((q => r) => (p => r)) in IPC-Taut
 (q => r) => ((p => q) => (p => r)) in IPC-Taut by Th22;
hence  (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th23; ::_thesis: verum
end;

theorem Th25: :: INTPRO_1:25
for p, q, r being Element of MC-wff st p => q in IPC-Taut holds
(q => r) => (p => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut )
assume A1: p => q in IPC-Taut ; ::_thesis: (q => r) => (p => r) in IPC-Taut
 (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
hence  (q => r) => (p => r) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th26: :: INTPRO_1:26
for p, q, r being Element of MC-wff st p => q in IPC-Taut & q => r in IPC-Taut holds
p => r in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut )
assume that
A1: p => q in IPC-Taut and
A2: q => r in IPC-Taut ; ::_thesis: p => r in IPC-Taut
 (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
then  (q => r) => (p => r) in IPC-Taut by A1, Def14;
hence  p => r in IPC-Taut by A2, Def14; ::_thesis: verum
end;

Lm4:  for q, r, p, s being Element of MC-wff holds (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
proof
let q, r, p, s be Element of MC-wff ; ::_thesis: (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
 (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
hence  (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut by Th25; ::_thesis: verum
end;

theorem Th27: :: INTPRO_1:27
for p, q, r, s being Element of MC-wff holds (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut
proof
let p, q, r, s be Element of MC-wff ; ::_thesis: (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut
A1: (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in IPC-Taut by Lm4;
 ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in IPC-Taut by Lm4;
hence  (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:28
for p, q, r being Element of MC-wff holds ((p => q) => r) => (q => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ((p => q) => r) => (q => r) in IPC-Taut
A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut by Th24;
 q => (p => q) in IPC-Taut by Def14;
hence  ((p => q) => r) => (q => r) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th29: :: INTPRO_1:29
for p, q, r being Element of MC-wff holds (p => (q => r)) => (q => (p => r)) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: (p => (q => r)) => (q => (p => r)) in IPC-Taut
A1: q => (p => q) in IPC-Taut by Def14;
 (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then A2: (p => q) => ((p => (q => r)) => (p => r)) in IPC-Taut by Th23;
 ((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in IPC-Taut by Th22;
then  (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A2, Def14;
then  q => ((p => (q => r)) => (p => r)) in IPC-Taut by A1, Def14;
hence  (p => (q => r)) => (q => (p => r)) in IPC-Taut by Th23; ::_thesis: verum
end;

theorem Th30: :: INTPRO_1:30
for p, q being Element of MC-wff holds (p => (p => q)) => (p => q) in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: (p => (p => q)) => (p => q) in IPC-Taut
 (p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14;
then A1: (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23;
 p => p in IPC-Taut by Th17;
hence  (p => (p => q)) => (p => q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:31
for q, p being Element of MC-wff holds q => ((q => p) => p) in IPC-Taut
proof
let q, p be Element of MC-wff ; ::_thesis: q => ((q => p) => p) in IPC-Taut
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29;
 (q => p) => (q => p) in IPC-Taut by Th17;
hence  q => ((q => p) => p) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th32: :: INTPRO_1:32
for s, q, p being Element of MC-wff st s => (q => p) in IPC-Taut & q in IPC-Taut holds
s => p in IPC-Taut
proof
let s, q, p be Element of MC-wff ; ::_thesis: ( s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut )
assume that
A1: s => (q => p) in IPC-Taut and
A2: q in IPC-Taut ; ::_thesis: s => p in IPC-Taut
 (s => (q => p)) => (q => (s => p)) in IPC-Taut by Th29;
then  q => (s => p) in IPC-Taut by A1, Def14;
hence  s => p in IPC-Taut by A2, Def14; ::_thesis: verum
end;

begin

theorem Th33: :: INTPRO_1:33
for p being Element of MC-wff holds p => (p '&' p) in IPC-Taut
proof
let p be Element of MC-wff ; ::_thesis: p => (p '&' p) in IPC-Taut
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30;
 p => (p => (p '&' p)) in IPC-Taut by Def14;
hence  p => (p '&' p) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th34: :: INTPRO_1:34
for p, q being Element of MC-wff holds
( p '&' q in IPC-Taut iff ( p in IPC-Taut & q in IPC-Taut ) )
proof
let p, q be Element of MC-wff ; ::_thesis: ( p '&' q in IPC-Taut iff ( p in IPC-Taut & q in IPC-Taut ) )
hereby  ::_thesis: ( p in IPC-Taut & q in IPC-Taut implies p '&' q in IPC-Taut )
A1: (p '&' q) => q in IPC-Taut by Def14;
assume A2: p '&' q in IPC-Taut ; ::_thesis: ( p in IPC-Taut & q in IPC-Taut )
 (p '&' q) => p in IPC-Taut by Def14;
hence  ( p in IPC-Taut & q in IPC-Taut ) by A2, A1, Def14; ::_thesis: verum
end;
assume that
A3: p in IPC-Taut and
A4: q in IPC-Taut ; ::_thesis: p '&' q in IPC-Taut
 p => (q => (p '&' q)) in IPC-Taut by Def14;
then  q => (p '&' q) in IPC-Taut by A3, Def14;
hence  p '&' q in IPC-Taut by A4, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:35
for p, q being Element of MC-wff holds
( p '&' q in IPC-Taut iff q '&' p in IPC-Taut )
proof
let p, q be Element of MC-wff ; ::_thesis: ( p '&' q in IPC-Taut iff q '&' p in IPC-Taut )
hereby  ::_thesis: ( q '&' p in IPC-Taut implies p '&' q in IPC-Taut )
assume A1: p '&' q in IPC-Taut ; ::_thesis: q '&' p in IPC-Taut
then A2: q in IPC-Taut by Th34;
 p in IPC-Taut by A1, Th34;
hence  q '&' p in IPC-Taut by A2, Th34; ::_thesis: verum
end;
assume A3: q '&' p in IPC-Taut ; ::_thesis: p '&' q in IPC-Taut
then A4: p in IPC-Taut by Th34;
 q in IPC-Taut by A3, Th34;
hence  p '&' q in IPC-Taut by A4, Th34; ::_thesis: verum
end;

theorem Th36: :: INTPRO_1:36
for p, q, r being Element of MC-wff holds ((p '&' q) => r) => (p => (q => r)) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in IPC-Taut
set qp = q => (p '&' q);
set pr = ((p '&' q) => r) => (q => r);
A1: (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) => ((p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r)))) in IPC-Taut by Def14;
A2: p => (q => (p '&' q)) in IPC-Taut by Def14;
 p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r))) in IPC-Taut by Th18, Th24;
then  (p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r))) in IPC-Taut by A1, Def14;
then A3: p => (((p '&' q) => r) => (q => r)) in IPC-Taut by A2, Def14;
 (p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r))) in IPC-Taut by Th29;
hence  ((p '&' q) => r) => (p => (q => r)) in IPC-Taut by A3, Def14; ::_thesis: verum
end;

theorem Th37: :: INTPRO_1:37
for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p '&' q) => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in IPC-Taut
A1: ((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in IPC-Taut by Th24;
 (p '&' q) => q in IPC-Taut by Def14;
then  (q => r) => ((p '&' q) => r) in IPC-Taut by A1, Def14;
then A2: p => ((q => r) => ((p '&' q) => r)) in IPC-Taut by Th18;
A3: (p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in IPC-Taut by Th29;
 (p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in IPC-Taut by Def14;
then  (p => (q => r)) => (p => ((p '&' q) => r)) in IPC-Taut by A2, Def14;
then A4: (p => (q => r)) => ((p '&' q) => (p => r)) in IPC-Taut by A3, Th26;
A5: (p '&' q) => p in IPC-Taut by Def14;
 ((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in IPC-Taut by Def14;
then  ((p '&' q) => (p => r)) => ((p '&' q) => r) in IPC-Taut by A5, Th32;
hence  (p => (q => r)) => ((p '&' q) => r) in IPC-Taut by A4, Th26; ::_thesis: verum
end;

theorem Th38: :: INTPRO_1:38
for r, p, q being Element of MC-wff holds (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut
proof
let r, p, q be Element of MC-wff ; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut
A1: (r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in IPC-Taut by Def14;
 p => (q => (p '&' q)) in IPC-Taut by Def14;
then A2: r => (p => (q => (p '&' q))) in IPC-Taut by Th18;
 (r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in IPC-Taut by Def14;
then  (r => p) => (r => (q => (p '&' q))) in IPC-Taut by A2, Def14;
hence  (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

theorem Th39: :: INTPRO_1:39
for p, q being Element of MC-wff holds ((p => q) '&' p) => q in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: ((p => q) '&' p) => q in IPC-Taut
set P = p => q;
A1: (p => q) => (p => q) in IPC-Taut by Th17;
 ((p => q) => (p => q)) => (((p => q) '&' p) => q) in IPC-Taut by Th37;
hence  ((p => q) '&' p) => q in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:40
for p, q, s being Element of MC-wff holds (((p => q) '&' p) '&' s) => q in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (((p => q) '&' p) '&' s) => q in IPC-Taut
set P = (p => q) '&' p;
A1: ((p => q) '&' p) => q in IPC-Taut by Th39;
 (((p => q) '&' p) '&' s) => ((p => q) '&' p) in IPC-Taut by Def14;
hence  (((p => q) '&' p) '&' s) => q in IPC-Taut by A1, Th26; ::_thesis: verum
end;

theorem :: INTPRO_1:41
for q, s, p being Element of MC-wff holds (q => s) => ((p '&' q) => s) in IPC-Taut
proof
let q, s, p be Element of MC-wff ; ::_thesis: (q => s) => ((p '&' q) => s) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => q in IPC-Taut by Def14;
 ((p '&' q) => q) => ((q => s) => ((p '&' q) => s)) in IPC-Taut by Th24;
hence  (q => s) => ((p '&' q) => s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th42: :: INTPRO_1:42
for q, s, p being Element of MC-wff holds (q => s) => ((q '&' p) => s) in IPC-Taut
proof
let q, s, p be Element of MC-wff ; ::_thesis: (q => s) => ((q '&' p) => s) in IPC-Taut
set P = q '&' p;
A1: (q '&' p) => q in IPC-Taut by Def14;
 ((q '&' p) => q) => ((q => s) => ((q '&' p) => s)) in IPC-Taut by Th24;
hence  (q => s) => ((q '&' p) => s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th43: :: INTPRO_1:43
for p, s, q being Element of MC-wff holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
set P = p '&' s;
A1: ((p '&' s) => q) => (((p '&' s) => s) => ((p '&' s) => (q '&' s))) in IPC-Taut by Th38;
 (p '&' s) => s in IPC-Taut by Def14;
hence  ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by A1, Th32; ::_thesis: verum
end;

theorem Th44: :: INTPRO_1:44
for p, q, s being Element of MC-wff holds (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
A1: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43;
 (p => q) => ((p '&' s) => q) in IPC-Taut by Th42;
hence  (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

theorem Th45: :: INTPRO_1:45
for p, q, s being Element of MC-wff holds ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut
set P = p => q;
set Q = p '&' s;
set S = q '&' s;
A1: (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th44;
 ((p => q) => ((p '&' s) => (q '&' s))) => (((p => q) '&' (p '&' s)) => (q '&' s)) in IPC-Taut by Th37;
hence  ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th46: :: INTPRO_1:46
for p, q being Element of MC-wff holds (p '&' q) => (q '&' p) in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: (p '&' q) => (q '&' p) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => q in IPC-Taut by Def14;
A2: (p '&' q) => p in IPC-Taut by Def14;
 ((p '&' q) => q) => (((p '&' q) => p) => ((p '&' q) => (q '&' p))) in IPC-Taut by Th38;
then  ((p '&' q) => p) => ((p '&' q) => (q '&' p)) in IPC-Taut by A1, Def14;
hence  (p '&' q) => (q '&' p) in IPC-Taut by A2, Def14; ::_thesis: verum
end;

theorem Th47: :: INTPRO_1:47
for p, q, s being Element of MC-wff holds ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut
A1: (q '&' s) => (s '&' q) in IPC-Taut by Th46;
 ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut by Th45;
hence  ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

theorem Th48: :: INTPRO_1:48
for p, q, s being Element of MC-wff holds (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
A1: ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut by Th47;
 (((p => q) '&' (p '&' s)) => (s '&' q)) => ((p => q) => ((p '&' s) => (s '&' q))) in IPC-Taut by Th36;
hence  (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th49: :: INTPRO_1:49
for p, q, s being Element of MC-wff holds (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
set T = s '&' p;
A1: (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut by Th48;
A2: (s '&' p) => (p '&' s) in IPC-Taut by Th46;
 ((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in IPC-Taut by Th27;
then  ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in IPC-Taut by A1, Def14;
hence  (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut by A2, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:50
for p, s, q being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in IPC-Taut by Th46;
 ((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut by Th49;
hence  (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:51
for p, q, s being Element of MC-wff holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p => q) '&' (p => s)) => (p => (q '&' s)) in IPC-Taut
set P = p => q;
set Q = p => s;
set S = p => (q '&' s);
A1: (p => q) => ((p => s) => (p => (q '&' s))) in IPC-Taut by Th38;
 ((p => q) => ((p => s) => (p => (q '&' s)))) => (((p => q) '&' (p => s)) => (p => (q '&' s))) in IPC-Taut by Th37;
hence  ((p => q) '&' (p => s)) => (p => (q '&' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

Lm5:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => q in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => q in IPC-Taut
A1: (p '&' q) => q in IPC-Taut by Def14;
 ((p '&' q) '&' s) => (p '&' q) in IPC-Taut by Def14;
hence  ((p '&' q) '&' s) => q in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm6:  for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
set P = (p '&' q) '&' s;
A1: ((p '&' q) '&' s) => q in IPC-Taut by Lm5;
 (((p '&' q) '&' s) => q) => ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in IPC-Taut by Th49;
hence  (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

Lm7:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
A1: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut by Lm6;
 ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) in IPC-Taut by Th33;
hence  ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm8:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => p in IPC-Taut by Def14;
 ((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in IPC-Taut by Th44;
hence  ((p '&' q) '&' s) => (p '&' s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

Lm9:  for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
set P = (p '&' q) '&' s;
set Q = p '&' s;
A1: ((p '&' q) '&' s) => (p '&' s) in IPC-Taut by Lm8;
 (((p '&' q) '&' s) => (p '&' s)) => ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in IPC-Taut by Th44;
hence  (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

Lm10:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
A1: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut by Lm9;
 ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut by Lm7;
hence  ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm11:  for p, s, q being Element of MC-wff holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
set P = p '&' s;
set Q = s '&' p;
A1: (p '&' s) => (s '&' p) in IPC-Taut by Th46;
 ((p '&' s) => (s '&' p)) => (((p '&' s) '&' q) => ((s '&' p) '&' q)) in IPC-Taut by Th44;
hence  ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

Lm12:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
A1: ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut by Lm11;
 ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut by Lm10;
hence  ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm13:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
A1: ((s '&' p) '&' q) => ((s '&' q) '&' p) in IPC-Taut by Lm10;
 ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut by Lm12;
hence  ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm14:  for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
A1: ((s '&' q) '&' p) => (p '&' (s '&' q)) in IPC-Taut by Th46;
 ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut by Lm13;
hence  ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm15:  for p, s, q being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in IPC-Taut by Th46;
 ((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut by Th49;
hence  (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:52
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (p '&' (q '&' s)) in IPC-Taut
A1: (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut by Lm15;
 ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut by Lm14;
hence  ((p '&' q) '&' s) => (p '&' (q '&' s)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm16:  for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
A1: (p '&' (s '&' q)) => ((s '&' q) '&' p) in IPC-Taut by Th46;
 (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by Lm15;
hence  (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm17:  for s, q, p being Element of MC-wff holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
proof
let s, q, p be Element of MC-wff ; ::_thesis: ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in IPC-Taut by Th46;
 ((s '&' q) => (q '&' s)) => (((s '&' q) '&' p) => ((q '&' s) '&' p)) in IPC-Taut by Th44;
hence  ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

Lm18:  for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
A1: ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut by Lm17;
 (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut by Lm16;
hence  (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm19:  for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
A1: ((q '&' s) '&' p) => ((p '&' s) '&' q) in IPC-Taut by Lm13;
 (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut by Lm18;
hence  (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

Lm20:  for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
set P = q '&' s;
set Q = s '&' q;
A1: (q '&' s) => (s '&' q) in IPC-Taut by Th46;
 ((q '&' s) => (s '&' q)) => ((p '&' (q '&' s)) => (p '&' (s '&' q))) in IPC-Taut by Th49;
hence  (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:53
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut
A1: (p '&' (s '&' q)) => ((p '&' q) '&' s) in IPC-Taut by Lm19;
 (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by Lm20;
hence  (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

begin

theorem Th54: :: INTPRO_1:54
for p being Element of MC-wff holds (p 'or' p) => p in IPC-Taut
proof
let p be Element of MC-wff ; ::_thesis: (p 'or' p) => p in IPC-Taut
A1: p => p in IPC-Taut by Th17;
 (p => p) => ((p => p) => ((p 'or' p) => p)) in IPC-Taut by Def14;
then  (p => p) => ((p 'or' p) => p) in IPC-Taut by A1, Def14;
hence  (p 'or' p) => p in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:55
for p, q being Element of MC-wff st ( p in IPC-Taut or q in IPC-Taut ) holds
p 'or' q in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: ( ( p in IPC-Taut or q in IPC-Taut ) implies p 'or' q in IPC-Taut )
assume A1: ( p in IPC-Taut or q in IPC-Taut ) ; ::_thesis: p 'or' q in IPC-Taut
now__::_thesis:_(_(_p_in_IPC-Taut_&_p_'or'_q_in_IPC-Taut_)_or_(_q_in_IPC-Taut_&_p_'or'_q_in_IPC-Taut_)_)
percases ( p in IPC-Taut or q in IPC-Taut ) by A1;
caseA2: p in IPC-Taut ; ::_thesis: p 'or' q in IPC-Taut
 p => (p 'or' q) in IPC-Taut by Def14;
hence  p 'or' q in IPC-Taut by A2, Def14; ::_thesis: verum
end;
caseA3: q in IPC-Taut ; ::_thesis: p 'or' q in IPC-Taut
 q => (p 'or' q) in IPC-Taut by Def14;
hence  p 'or' q in IPC-Taut by A3, Def14; ::_thesis: verum
end;
end;
end;
hence  p 'or' q in IPC-Taut ; ::_thesis: verum
end;

theorem Th56: :: INTPRO_1:56
for p, q being Element of MC-wff holds (p 'or' q) => (q 'or' p) in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: (p 'or' q) => (q 'or' p) in IPC-Taut
A1: p => (q 'or' p) in IPC-Taut by Def14;
A2: q => (q 'or' p) in IPC-Taut by Def14;
 (p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by Def14;
then  (q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)) in IPC-Taut by A1, Def14;
hence  (p 'or' q) => (q 'or' p) in IPC-Taut by A2, Def14; ::_thesis: verum
end;

theorem :: INTPRO_1:57
for p, q being Element of MC-wff holds
( p 'or' q in IPC-Taut iff q 'or' p in IPC-Taut )
proof
let p, q be Element of MC-wff ; ::_thesis: ( p 'or' q in IPC-Taut iff q 'or' p in IPC-Taut )
hereby  ::_thesis: ( q 'or' p in IPC-Taut implies p 'or' q in IPC-Taut )
assume A1: p 'or' q in IPC-Taut ; ::_thesis: q 'or' p in IPC-Taut
 (p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
hence  q 'or' p in IPC-Taut by A1, Def14; ::_thesis: verum
end;
assume A2: q 'or' p in IPC-Taut ; ::_thesis: p 'or' q in IPC-Taut
 (q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
hence  p 'or' q in IPC-Taut by A2, Def14; ::_thesis: verum
end;

theorem Th58: :: INTPRO_1:58
for p, q, s being Element of MC-wff holds (p => q) => (p => (q 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => (p => (q 'or' s)) in IPC-Taut
A1: (q => (q 'or' s)) => ((p => q) => (p => (q 'or' s))) in IPC-Taut by Th22;
 q => (q 'or' s) in IPC-Taut by Def14;
hence  (p => q) => (p => (q 'or' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th59: :: INTPRO_1:59
for p, q, s being Element of MC-wff holds (p => q) => (p => (s 'or' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => (p => (s 'or' q)) in IPC-Taut
A1: (q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22;
 q => (s 'or' q) in IPC-Taut by Def14;
hence  (p => q) => (p => (s 'or' q)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th60: :: INTPRO_1:60
for p, q, s being Element of MC-wff holds (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut
set P = p 'or' s;
set Q = q 'or' s;
A1: (p => q) => (p => (q 'or' s)) in IPC-Taut by Th58;
 (p => (q 'or' s)) => ((s => (q 'or' s)) => ((p 'or' s) => (q 'or' s))) in IPC-Taut by Def14;
then A2: (s => (q 'or' s)) => ((p => (q 'or' s)) => ((p 'or' s) => (q 'or' s))) in IPC-Taut by Th23;
 s => (q 'or' s) in IPC-Taut by Def14;
then  (p => (q 'or' s)) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by A2, Def14;
hence  (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

theorem Th61: :: INTPRO_1:61
for p, q, s being Element of MC-wff st p => q in IPC-Taut holds
(p 'or' s) => (q 'or' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut )
assume A1: p => q in IPC-Taut ; ::_thesis: (p 'or' s) => (q 'or' s) in IPC-Taut
 (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by Th60;
hence  (p 'or' s) => (q 'or' s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th62: :: INTPRO_1:62
for p, q, s being Element of MC-wff holds (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut
set P = s 'or' p;
set Q = s 'or' q;
A1: s => (s 'or' q) in IPC-Taut by Def14;
A2: (p => q) => (p => (s 'or' q)) in IPC-Taut by Th59;
 (s => (s 'or' q)) => ((p => (s 'or' q)) => ((s 'or' p) => (s 'or' q))) in IPC-Taut by Def14;
then  (p => (s 'or' q)) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by A1, Def14;
hence  (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by A2, Th26; ::_thesis: verum
end;

theorem Th63: :: INTPRO_1:63
for p, q, s being Element of MC-wff st p => q in IPC-Taut holds
(s 'or' p) => (s 'or' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut implies (s 'or' p) => (s 'or' q) in IPC-Taut )
assume A1: p => q in IPC-Taut ; ::_thesis: (s 'or' p) => (s 'or' q) in IPC-Taut
 (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by Th62;
hence  (s 'or' p) => (s 'or' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;

theorem Th64: :: INTPRO_1:64
for p, q, s being Element of MC-wff holds (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut
set P = p 'or' s;
set Q = q 'or' s;
A1: (p 'or' s) => (q 'or' (p 'or' s)) in IPC-Taut by Def14;
 p => (p 'or' s) in IPC-Taut by Def14;
then  p => (q 'or' (p 'or' s)) in IPC-Taut by A1, Th26;
then A2: ((q 'or' (p 'or' s)) 'or' p) => ((q 'or' (p 'or' s)) 'or' (q 'or' (p 'or' s))) in IPC-Taut by Th63;
 ((q 'or' (p 'or' s)) 'or' (q 'or' (p 'or' s))) => (q 'or' (p 'or' s)) in IPC-Taut by Th54;
then A3: ((q 'or' (p 'or' s)) 'or' p) => (q 'or' (p 'or' s)) in IPC-Taut by A2, Th26;
 s => (p 'or' s) in IPC-Taut by Def14;
then  (q 'or' s) => (q 'or' (p 'or' s)) in IPC-Taut by Th63;
then A4: (p 'or' (q 'or' s)) => (p 'or' (q 'or' (p 'or' s))) in IPC-Taut by Th63;
 (p 'or' (q 'or' (p 'or' s))) => ((q 'or' (p 'or' s)) 'or' p) in IPC-Taut by Th56;
then  (p 'or' (q 'or' s)) => ((q 'or' (p 'or' s)) 'or' p) in IPC-Taut by A4, Th26;
hence  (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut by A3, Th26; ::_thesis: verum
end;

theorem :: INTPRO_1:65
for p, q, s being Element of MC-wff holds (p 'or' (q 'or' s)) => ((p 'or' q) 'or' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p 'or' (q 'or' s)) => ((p 'or' q) 'or' s) in IPC-Taut
A1: (s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56;
 (q 'or' s) => (s 'or' q) in IPC-Taut by Th56;
then A2: (p 'or' (q 'or' s)) => (p 'or' (s 'or' q)) in IPC-Taut by Th63;
 (p 'or' (s 'or' q)) => (s 'or' (p 'or' q)) in IPC-Taut by Th64;
then  (p 'or' (q 'or' s)) => (s 'or' (p 'or' q)) in IPC-Taut by A2, Th26;
hence  (p 'or' (q 'or' s)) => ((p 'or' q) 'or' s) in IPC-Taut by A1, Th26; ::_thesis: verum
end;

theorem :: INTPRO_1:66
for p, q, s being Element of MC-wff holds ((p 'or' q) 'or' s) => (p 'or' (q 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p 'or' q) 'or' s) => (p 'or' (q 'or' s)) in IPC-Taut
 (p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
then A1: ((p 'or' q) 'or' s) => ((q 'or' p) 'or' s) in IPC-Taut by Th61;
 (q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
then A2: (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63;
 ((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56;
then  ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1, Th26;
then A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2, Th26;
 (s 'or' q) => (q 'or' s) in IPC-Taut by Th56;
then A4: (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63;
 (s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64;
then  ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3, Th26;
hence  ((p 'or' q) 'or' s) => (p 'or' (q 'or' s)) in IPC-Taut by A4, Th26; ::_thesis: verum
end;

begin


definition
let T be Subset of MC-wff;
attrT is CPC_theory  means :Def19: :: INTPRO_1:def 19
 for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) );
correctness
;
end;

:: deftheorem Def19 defines CPC_theory INTPRO_1:def_19_:_
 for T being Subset of MC-wff holds
( T is CPC_theory iff for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) ) );

theorem Th67: :: INTPRO_1:67
for T being Subset of MC-wff st T is CPC_theory holds
T is IPC_theory
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory implies T is IPC_theory )
assume A1: T is CPC_theory ; ::_thesis: T is IPC_theory
let p, q, r be Element of MC-wff ; :: according to INTPRO_1:def_14 ::_thesis: ( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) )
thus  ( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) by A1, Def19; ::_thesis: verum
end;

definition
let X be Subset of MC-wff;
func CnCPC X ->  Subset of MC-wff means :Def20: :: INTPRO_1:def 20
 for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T );
existence
 ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means  for T being Subset of MC-wff st T is CPC_theory & X c= T holds
$1 in T;
consider Y being set  such that
A1: for a being set holds
( a in Y iff ( a in MC-wff & S1[a] ) ) from XBOOLE_0:sch_1();
 Y c= MC-wff
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in MC-wff )
assume  a in Y ; ::_thesis: a in MC-wff
hence  a in MC-wff by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of MC-wff ;
take  Z ; ::_thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T )
thus  for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of MC-wff; ::_thesis: ( ( for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) and
A3: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ; ::_thesis: Y = Z
 for a being set holds
( a in Y iff a in Z )
proof
let a be set ; ::_thesis: ( a in Y iff a in Z )
hereby  ::_thesis: ( a in Z implies a in Y )
assume A4: a in Y ; ::_thesis: a in Z
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is CPC_theory & X c= T holds
t in T by A2, A4;
hence  a in Z by A3; ::_thesis: verum
end;
assume A5: a in Z ; ::_thesis: a in Y
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is CPC_theory & X c= T holds
t in T by A3, A5;
hence  a in Y by A2; ::_thesis: verum
end;
hence  Y = Z by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines CnCPC INTPRO_1:def_20_:_
 for X, b2 being Subset of MC-wff holds
( b2 = CnCPC X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) );

definition
func CPC-Taut  ->  Subset of MC-wff equals :: INTPRO_1:def 21
 CnCPC ({} MC-wff);
correctness
coherence
CnCPC ({} MC-wff) is Subset of MC-wff;
;
end;

:: deftheorem  defines CPC-Taut INTPRO_1:def_21_:_
 CPC-Taut = CnCPC ({} MC-wff);

theorem Th68: :: INTPRO_1:68
for X being Subset of MC-wff holds CnIPC X c= CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC X c= CnCPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC X or a in CnCPC X )
assume A1: a in CnIPC X ; ::_thesis: a in CnCPC X
then reconsider r = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies r in T )
assume that
A2: T is CPC_theory and
A3: X c= T ; ::_thesis: r in T
 T is IPC_theory by A2, Th67;
hence  r in T by A1, A3, Def15; ::_thesis: verum
end;
hence  a in CnCPC X by Def20; ::_thesis: verum
end;

theorem Th69: :: INTPRO_1:69
for X being Subset of MC-wff
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 )
proof
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 by Def19;
hence  p 'or' (p => FALSUM) in CnCPC X by Def20; ::_thesis: verum
end;

theorem Th70: :: INTPRO_1:70
for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnCPC X & p => q in CnCPC X holds
q in CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff st p in CnCPC X & p => q in CnCPC X holds
q in CnCPC X
let p, q be Element of MC-wff ; ::_thesis: ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X )
assume that
A1: p in CnCPC X and
A2: p => q in CnCPC X ; ::_thesis: q in CnCPC X
 for T being Subset of MC-wff st T is CPC_theory & X c= T holds
q in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies q in T )
assume that
A3: T is CPC_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def20;
 p in T by A1, A3, A4, Def20;
hence  q in T by A3, A5, Def19; ::_thesis: verum
end;
hence  q in CnCPC X by Def20; ::_thesis: verum
end;

theorem Th71: :: INTPRO_1:71
for T, X being Subset of MC-wff st T is CPC_theory & X c= T holds
CnCPC X c= T
proof
let T, X be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies CnCPC X c= T )
assume that
A1: T is CPC_theory and
A2: X c= T ; ::_thesis: CnCPC X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC X or a in T )
thus  ( not a in CnCPC X or a in T ) by A1, A2, Def20; ::_thesis: verum
end;

theorem Th72: :: INTPRO_1:72
for X being Subset of MC-wff holds X c= CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: X c= CnCPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnCPC X )
assume A1: a in X ; ::_thesis: a in CnCPC X
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is CPC_theory & X c= T holds
t in T by A1;
hence  a in CnCPC X by Def20; ::_thesis: verum
end;

theorem Th73: :: INTPRO_1:73
for X, Y being Subset of MC-wff st X c= Y holds
CnCPC X c= CnCPC Y
proof
let X, Y be Subset of MC-wff; ::_thesis: ( X c= Y implies CnCPC X c= CnCPC Y )
assume A1: X c= Y ; ::_thesis: CnCPC X c= CnCPC Y
thus  CnCPC X c= CnCPC Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC X or a in CnCPC Y )
assume A2: a in CnCPC X ; ::_thesis: a in CnCPC Y
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is CPC_theory & Y c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & Y c= T implies t in T )
assume that
A3: T is CPC_theory and
A4: Y c= T ; ::_thesis: t in T
 X c= T by A1, A4, XBOOLE_1:1;
hence  t in T by A2, A3, Def20; ::_thesis: verum
end;
hence  a in CnCPC Y by Def20; ::_thesis: verum
end;
end;

Lm21:  for X being Subset of MC-wff holds CnCPC (CnCPC X) c= CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: CnCPC (CnCPC X) c= CnCPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC (CnCPC X) or a in CnCPC X )
assume A1: a in CnCPC (CnCPC X) ; ::_thesis: a in CnCPC X
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is CPC_theory & X c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies t in T )
assume that
A2: T is CPC_theory and
A3: X c= T ; ::_thesis: t in T
 CnCPC X c= T by A2, A3, Th71;
hence  t in T by A1, A2, Def20; ::_thesis: verum
end;
hence  a in CnCPC X by Def20; ::_thesis: verum
end;

theorem :: INTPRO_1:74
for X being Subset of MC-wff holds CnCPC (CnCPC X) = CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: CnCPC (CnCPC X) = CnCPC X
A1: CnCPC X c= CnCPC (CnCPC X) by Th72;
 CnCPC (CnCPC X) c= CnCPC X by Lm21;
hence  CnCPC (CnCPC X) = CnCPC X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm22:  for X being Subset of MC-wff holds CnCPC X is CPC_theory
proof
let X be Subset of MC-wff; ::_thesis: CnCPC X is CPC_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def_19 ::_thesis: for 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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
let 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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  p => (q => p) in CnCPC X by Th69; ::_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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X by Th69; ::_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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  (p '&' q) => p in CnCPC X by Th69; ::_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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  (p '&' q) => q in CnCPC X by Th69; ::_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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  p => (q => (p '&' q)) in CnCPC X by Th69; ::_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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  p => (p 'or' q) in CnCPC X by Th69; ::_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 & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  q => (p 'or' q) in CnCPC X by Th69; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X by Th69; ::_thesis: ( FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  FALSUM => p in CnCPC X by Th69; ::_thesis: ( p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus  p 'or' (p => FALSUM) in CnCPC X by Th69; ::_thesis: ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X )
thus  ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) by Th70; ::_thesis: verum
end;

registration
let X be Subset of MC-wff;
cluster CnCPC X ->  CPC_theory ;
coherence
 CnCPC X is CPC_theory by Lm22;
end;

theorem Th75: :: INTPRO_1:75
for T being Subset of MC-wff holds
( T is CPC_theory iff CnCPC T = T )
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory iff CnCPC T = T )
hereby  ::_thesis: ( CnCPC T = T implies T is CPC_theory )
assume A1: T is CPC_theory ; ::_thesis: CnCPC T = T
A2: CnCPC T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC T or a in T )
assume  a in CnCPC T ; ::_thesis: a in T
hence  a in T by A1, Def20; ::_thesis: verum
end;
 T c= CnCPC T by Th72;
hence  CnCPC T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( CnCPC T = T implies T is CPC_theory ) ; ::_thesis: verum
end;

theorem :: INTPRO_1:76
for T being Subset of MC-wff st T is CPC_theory holds
CPC-Taut c= T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory implies CPC-Taut c= T )
assume A1: T is CPC_theory ; ::_thesis: CPC-Taut c= T
 CPC-Taut c= CnCPC T by Th73, XBOOLE_1:2;
hence  CPC-Taut c= T by A1, Th75; ::_thesis: verum
end;

registration
cluster CPC-Taut  ->  CPC_theory ;
coherence
 CPC-Taut is CPC_theory ;
end;

theorem :: INTPRO_1:77
IPC-Taut c= CPC-Taut by Th68;

begin


definition
let T be Subset of MC-wff;
attrT is S4_theory  means :Def22: :: INTPRO_1:def 22
 for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) => (Nes q)) in T & (Nes p) => p in T & (Nes p) => (Nes (Nes p)) in T & ( p in T & p => q in T implies q in T ) & ( p in T implies Nes p in T ) );
correctness
;
end;

:: deftheorem Def22 defines S4_theory INTPRO_1:def_22_:_
 for T being Subset of MC-wff holds
( T is S4_theory iff for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) => (Nes q)) in T & (Nes p) => p in T & (Nes p) => (Nes (Nes p)) in T & ( p in T & p => q in T implies q in T ) & ( p in T implies Nes p in T ) ) );

theorem Th78: :: INTPRO_1:78
for T being Subset of MC-wff st T is S4_theory holds
T is CPC_theory
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory implies T is CPC_theory )
assume A1: T is S4_theory ; ::_thesis: T is CPC_theory
let p, q, r be Element of MC-wff ; :: according to INTPRO_1:def_19 ::_thesis: ( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) )
thus  ( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) ) by A1, Def22; ::_thesis: verum
end;

theorem :: INTPRO_1:79
for T being Subset of MC-wff st T is S4_theory holds
T is IPC_theory
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory implies T is IPC_theory )
assume A1: T is S4_theory ; ::_thesis: T is IPC_theory
let p, q, r be Element of MC-wff ; :: according to INTPRO_1:def_14 ::_thesis: ( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) )
thus  ( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) by A1, Def22; ::_thesis: verum
end;

definition
let X be Subset of MC-wff;
func CnS4 X ->  Subset of MC-wff means :Def23: :: INTPRO_1:def 23
 for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T );
existence
 ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means  for T being Subset of MC-wff st T is S4_theory & X c= T holds
$1 in T;
consider Y being set  such that
A1: for a being set holds
( a in Y iff ( a in MC-wff & S1[a] ) ) from XBOOLE_0:sch_1();
 Y c= MC-wff
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in MC-wff )
assume  a in Y ; ::_thesis: a in MC-wff
hence  a in MC-wff by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of MC-wff ;
take  Z ; ::_thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )
thus  for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of MC-wff; ::_thesis: ( ( for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) and
A3: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ; ::_thesis: Y = Z
 for a being set holds
( a in Y iff a in Z )
proof
let a be set ; ::_thesis: ( a in Y iff a in Z )
hereby  ::_thesis: ( a in Z implies a in Y )
assume A4: a in Y ; ::_thesis: a in Z
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
t in T by A2, A4;
hence  a in Z by A3; ::_thesis: verum
end;
assume A5: a in Z ; ::_thesis: a in Y
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
t in T by A3, A5;
hence  a in Y by A2; ::_thesis: verum
end;
hence  Y = Z by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def23 defines CnS4 INTPRO_1:def_23_:_
 for X, b2 being Subset of MC-wff holds
( b2 = CnS4 X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) );

definition
func S4-Taut  ->  Subset of MC-wff equals :: INTPRO_1:def 24
 CnS4 ({} MC-wff);
correctness
coherence
CnS4 ({} MC-wff) is Subset of MC-wff;
;
end;

:: deftheorem  defines S4-Taut INTPRO_1:def_24_:_
 S4-Taut = CnS4 ({} MC-wff);

theorem Th80: :: INTPRO_1:80
for X being Subset of MC-wff holds CnCPC X c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnCPC X c= CnS4 X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC X or a in CnS4 X )
assume A1: a in CnCPC X ; ::_thesis: a in CnS4 X
then reconsider r = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies r in T )
assume that
A2: T is S4_theory and
A3: X c= T ; ::_thesis: r in T
 T is CPC_theory by A2, Th78;
hence  r in T by A1, A3, Def20; ::_thesis: verum
end;
hence  a in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th81: :: INTPRO_1:81
for X being Subset of MC-wff holds CnIPC X c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC X c= CnS4 X
A1: CnCPC X c= CnS4 X by Th80;
 CnIPC X c= CnCPC X by Th68;
hence  CnIPC X c= CnS4 X by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th82: :: INTPRO_1:82
for X being Subset of MC-wff
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 )
proof
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 by Def22;
hence  p 'or' (p => FALSUM) in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th83: :: INTPRO_1:83
for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnS4 X & p => q in CnS4 X holds
q in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff st p in CnS4 X & p => q in CnS4 X holds
q in CnS4 X
let p, q be Element of MC-wff ; ::_thesis: ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X )
assume that
A1: p in CnS4 X and
A2: p => q in CnS4 X ; ::_thesis: q in CnS4 X
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
q in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies q in T )
assume that
A3: T is S4_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def23;
 p in T by A1, A3, A4, Def23;
hence  q in T by A3, A5, Def22; ::_thesis: verum
end;
hence  q in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th84: :: INTPRO_1:84
for X being Subset of MC-wff
for p, q being Element of MC-wff holds (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X
let p, q be Element of MC-wff ; ::_thesis: (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
(Nes (p => q)) => ((Nes p) => (Nes q)) in T by Def22;
hence  (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th85: :: INTPRO_1:85
for X being Subset of MC-wff
for p being Element of MC-wff holds (Nes p) => p in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff holds (Nes p) => p in CnS4 X
let p be Element of MC-wff ; ::_thesis: (Nes p) => p in CnS4 X
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
(Nes p) => p in T by Def22;
hence  (Nes p) => p in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th86: :: INTPRO_1:86
for X being Subset of MC-wff
for p being Element of MC-wff holds (Nes p) => (Nes (Nes p)) in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff holds (Nes p) => (Nes (Nes p)) in CnS4 X
let p be Element of MC-wff ; ::_thesis: (Nes p) => (Nes (Nes p)) in CnS4 X
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
(Nes p) => (Nes (Nes p)) in T by Def22;
hence  (Nes p) => (Nes (Nes p)) in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th87: :: INTPRO_1:87
for X being Subset of MC-wff
for p being Element of MC-wff st p in CnS4 X holds
Nes p in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff st p in CnS4 X holds
Nes p in CnS4 X
let p be Element of MC-wff ; ::_thesis: ( p in CnS4 X implies Nes p in CnS4 X )
assume A1: p in CnS4 X ; ::_thesis: Nes p in CnS4 X
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
Nes p in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies Nes p in T )
assume that
A2: T is S4_theory and
A3: X c= T ; ::_thesis: Nes p in T
 p in T by A1, A2, A3, Def23;
hence  Nes p in T by A2, Def22; ::_thesis: verum
end;
hence  Nes p in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th88: :: INTPRO_1:88
for T, X being Subset of MC-wff st T is S4_theory & X c= T holds
CnS4 X c= T
proof
let T, X be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies CnS4 X c= T )
assume that
A1: T is S4_theory and
A2: X c= T ; ::_thesis: CnS4 X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 X or a in T )
thus  ( not a in CnS4 X or a in T ) by A1, A2, Def23; ::_thesis: verum
end;

theorem Th89: :: INTPRO_1:89
for X being Subset of MC-wff holds X c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: X c= CnS4 X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnS4 X )
assume A1: a in X ; ::_thesis: a in CnS4 X
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
t in T by A1;
hence  a in CnS4 X by Def23; ::_thesis: verum
end;

theorem Th90: :: INTPRO_1:90
for X, Y being Subset of MC-wff st X c= Y holds
CnS4 X c= CnS4 Y
proof
let X, Y be Subset of MC-wff; ::_thesis: ( X c= Y implies CnS4 X c= CnS4 Y )
assume A1: X c= Y ; ::_thesis: CnS4 X c= CnS4 Y
thus  CnS4 X c= CnS4 Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 X or a in CnS4 Y )
assume A2: a in CnS4 X ; ::_thesis: a in CnS4 Y
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is S4_theory & Y c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & Y c= T implies t in T )
assume that
A3: T is S4_theory and
A4: Y c= T ; ::_thesis: t in T
 X c= T by A1, A4, XBOOLE_1:1;
hence  t in T by A2, A3, Def23; ::_thesis: verum
end;
hence  a in CnS4 Y by Def23; ::_thesis: verum
end;
end;

Lm23:  for X being Subset of MC-wff holds CnS4 (CnS4 X) c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnS4 (CnS4 X) c= CnS4 X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 (CnS4 X) or a in CnS4 X )
assume A1: a in CnS4 (CnS4 X) ; ::_thesis: a in CnS4 X
then reconsider t = a as Element of MC-wff ;
 for T being Subset of MC-wff st T is S4_theory & X c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies t in T )
assume that
A2: T is S4_theory and
A3: X c= T ; ::_thesis: t in T
 CnS4 X c= T by A2, A3, Th88;
hence  t in T by A1, A2, Def23; ::_thesis: verum
end;
hence  a in CnS4 X by Def23; ::_thesis: verum
end;

theorem :: INTPRO_1:91
for X being Subset of MC-wff holds CnS4 (CnS4 X) = CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnS4 (CnS4 X) = CnS4 X
A1: CnS4 X c= CnS4 (CnS4 X) by Th89;
 CnS4 (CnS4 X) c= CnS4 X by Lm23;
hence  CnS4 (CnS4 X) = CnS4 X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm24:  for X being Subset of MC-wff holds CnS4 X is S4_theory
proof
let X be Subset of MC-wff; ::_thesis: CnS4 X is S4_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def_22 ::_thesis: for 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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
let 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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  p => (q => p) in CnS4 X by Th82; ::_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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X by Th82; ::_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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (p '&' q) => p in CnS4 X by Th82; ::_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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (p '&' q) => q in CnS4 X by Th82; ::_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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  p => (q => (p '&' q)) in CnS4 X by Th82; ::_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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  p => (p 'or' q) in CnS4 X by Th82; ::_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 & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  q => (p 'or' q) in CnS4 X by Th82; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X by Th82; ::_thesis: ( FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  FALSUM => p in CnS4 X by Th82; ::_thesis: ( p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  p 'or' (p => FALSUM) in CnS4 X by Th82; ::_thesis: ( (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X by Th84; ::_thesis: ( (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (Nes p) => p in CnS4 X by Th85; ::_thesis: ( (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  (Nes p) => (Nes (Nes p)) in CnS4 X by Th86; ::_thesis: ( ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus  ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) by Th83; ::_thesis: ( p in CnS4 X implies Nes p in CnS4 X )
thus  ( p in CnS4 X implies Nes p in CnS4 X ) by Th87; ::_thesis: verum
end;

registration
let X be Subset of MC-wff;
cluster CnS4 X ->  S4_theory ;
coherence
 CnS4 X is S4_theory by Lm24;
end;

theorem Th92: :: INTPRO_1:92
for T being Subset of MC-wff holds
( T is S4_theory iff CnS4 T = T )
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory iff CnS4 T = T )
hereby  ::_thesis: ( CnS4 T = T implies T is S4_theory )
assume A1: T is S4_theory ; ::_thesis: CnS4 T = T
A2: CnS4 T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 T or a in T )
assume  a in CnS4 T ; ::_thesis: a in T
hence  a in T by A1, Def23; ::_thesis: verum
end;
 T c= CnS4 T by Th89;
hence  CnS4 T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( CnS4 T = T implies T is S4_theory ) ; ::_thesis: verum
end;

theorem :: INTPRO_1:93
for T being Subset of MC-wff st T is S4_theory holds
S4-Taut c= T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory implies S4-Taut c= T )
assume A1: T is S4_theory ; ::_thesis: S4-Taut c= T
 S4-Taut c= CnS4 T by Th90, XBOOLE_1:2;
hence  S4-Taut c= T by A1, Th92; ::_thesis: verum
end;

registration
cluster S4-Taut  ->  S4_theory ;
coherence
 S4-Taut is S4_theory ;
end;

theorem :: INTPRO_1:94
CPC-Taut c= S4-Taut by Th80;

theorem :: INTPRO_1:95
IPC-Taut c= S4-Taut by Th81;