:: Suszko's Non-Fregean Logics, Part 1
:: by Taneli Huuskonen
::
:: Received December 2, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users


::
:: The Construction of Suszko's Sentential Calculus with Identity
::
definition
func VARS -> FinSequence-membered set equals :: SUSZKO_1:def 1
 { <*0,k*> where k is Element of NAT : verum } ;
coherence
{ <*0,k*> where k is Element of NAT : verum } is FinSequence-membered set
proof end;
end;

:: deftheorem defines VARS SUSZKO_1:def 1 :
VARS = { <*0,k*> where k is Element of NAT : verum } ;

registration
cluster VARS -> non empty FinSequence-membered antichain-like ;
coherence
( not VARS is empty & VARS is antichain-like )
proof end;
end;

definition
mode Variable is Element of VARS ;
end;

Lm1: for a being Variable holds
( 1 in dom a & a . 1 = 0 )
proof end;

:: definition
:: func TRUE -> FinSequence equals <*1*>;
:: coherence;
:: func FALSE -> FinSequence equals <*2*>;
:: coherence;
:: end;
definition
:: definition
:: func TRUE -> FinSequence equals <*1*>;
:: coherence;
:: func FALSE -> FinSequence equals <*2*>;
:: coherence;
:: end;
func 'not' -> FinSequence equals :: SUSZKO_1:def 2
<*11*>;
coherence
<*11*> is FinSequence ;
func '&&s' -> FinSequence equals :: SUSZKO_1:def 3
<*21*>;
coherence
<*21*> is FinSequence ;
func '||s' -> FinSequence equals :: SUSZKO_1:def 4
<*22*>;
coherence
<*22*> is FinSequence ;
end;

:: deftheorem defines 'not' SUSZKO_1:def 2 :
'not' = <*11*>;

:: deftheorem defines '&&s' SUSZKO_1:def 3 :
'&&s' = <*21*>;

:: deftheorem defines '||s' SUSZKO_1:def 4 :
'||s' = <*22*>;

definition
func '->' -> FinSequence equals :: SUSZKO_1:def 5
<*23*>;
coherence
<*23*> is FinSequence ;
func '<->' -> FinSequence equals :: SUSZKO_1:def 6
<*24*>;
coherence
<*24*> is FinSequence ;
func '==' -> FinSequence equals :: SUSZKO_1:def 7
<*25*>;
coherence
<*25*> is FinSequence ;
end;

:: deftheorem defines '->' SUSZKO_1:def 5 :
'->' = <*23*>;

:: deftheorem defines '<->' SUSZKO_1:def 6 :
'<->' = <*24*>;

:: deftheorem defines '==' SUSZKO_1:def 7 :
'==' = <*25*>;

definition
func SCI-unops -> non empty FinSequence-membered set equals :: SUSZKO_1:def 8
{'not'};
coherence
{'not'} is non empty FinSequence-membered set
proof end;
func SCI-binops -> non empty FinSequence-membered set equals :: SUSZKO_1:def 9
{'&&s','||s','->','<->','=='};
coherence
{'&&s','||s','->','<->','=='} is non empty FinSequence-membered set
proof end;
end;

:: deftheorem defines SCI-unops SUSZKO_1:def 8 :
SCI-unops = {'not'};

:: deftheorem defines SCI-binops SUSZKO_1:def 9 :
SCI-binops = {'&&s','||s','->','<->','=='};

theorem Th1: :: SUSZKO_1:1
for a being object holds
( ( a in SCI-unops implies a = 'not' ) & ( a = 'not' implies a in SCI-unops ) & ( not a in SCI-binops or a = '&&s' or a = '||s' or a = '->' or a = '<->' or a = '==' ) & ( ( a = '&&s' or a = '||s' or a = '->' or a = '<->' or a = '==' ) implies a in SCI-binops ) ) by TARSKI:def 1, ENUMSET1:def 3;

registration
let F, G be non empty FinSequence-membered set ;
cluster F \/ G -> non empty FinSequence-membered ;
coherence
( not F \/ G is empty & F \/ G is FinSequence-membered ) ;
end;

definition
func SCI-ops -> non empty FinSequence-membered set equals :: SUSZKO_1:def 10
SCI-unops \/ SCI-binops;
coherence
SCI-unops \/ SCI-binops is non empty FinSequence-membered set ;
end;

:: deftheorem defines SCI-ops SUSZKO_1:def 10 :
SCI-ops = SCI-unops \/ SCI-binops;

Lm3: for a being object holds
( a in SCI-ops iff ( a = 'not' or a = '&&s' or a = '||s' or a = '->' or a = '<->' or a = '==' ) )
proof end;

Lm4: for p being Element of SCI-ops holds
( dom p = Seg 1 & p . 1 <> 0 )
proof end;

theorem :: SUSZKO_1:2
for p being FinSequence holds
( ( p = 'not' implies p . 1 = 11 ) & ( p = '&&s' implies p . 1 = 21 ) & ( p = '||s' implies p . 1 = 22 ) & ( p = '->' implies p . 1 = 23 ) & ( p = '<->' implies p . 1 = 24 ) & ( p = '==' implies p . 1 = 25 ) ) ;

registration
cluster SCI-ops -> non empty FinSequence-membered antichain-like ;
coherence
( not SCI-ops is empty & SCI-ops is antichain-like )
proof end;
end;

definition
func SCI-symbols -> non empty FinSequence-membered set equals :: SUSZKO_1:def 11
VARS \/ SCI-ops;
coherence
VARS \/ SCI-ops is non empty FinSequence-membered set ;
end;

:: deftheorem defines SCI-symbols SUSZKO_1:def 11 :
SCI-symbols = VARS \/ SCI-ops;

definition
:: original: VARS
redefine func VARS -> non empty Subset of SCI-symbols;
coherence
VARS is non empty Subset of SCI-symbols by XBOOLE_1:7;
:: original: SCI-ops
redefine func SCI-ops -> non empty Subset of SCI-symbols;
coherence
SCI-ops is non empty Subset of SCI-symbols by XBOOLE_1:7;
:: original: SCI-unops
redefine func SCI-unops -> non empty Subset of SCI-symbols;
coherence
SCI-unops is non empty Subset of SCI-symbols by XBOOLE_1:7, XBOOLE_1:10;
:: original: SCI-binops
redefine func SCI-binops -> non empty Subset of SCI-symbols;
coherence
SCI-binops is non empty Subset of SCI-symbols by XBOOLE_1:7, XBOOLE_1:10;
end;

definition
:: original: 'not'
redefine func 'not' -> Element of SCI-symbols ;
coherence
'not' is Element of SCI-symbols
proof end;
:: original: '&&s'
redefine func '&&s' -> Element of SCI-symbols ;
coherence
'&&s' is Element of SCI-symbols
proof end;
:: original: '||s'
redefine func '||s' -> Element of SCI-symbols ;
coherence
'||s' is Element of SCI-symbols
proof end;
:: original: '->'
redefine func '->' -> Element of SCI-symbols ;
coherence
'->' is Element of SCI-symbols
proof end;
:: original: '<->'
redefine func '<->' -> Element of SCI-symbols ;
coherence
'<->' is Element of SCI-symbols
proof end;
:: original: '=='
redefine func '==' -> Element of SCI-symbols ;
coherence
'==' is Element of SCI-symbols
proof end;
end;

Lm5: for p being Element of SCI-symbols holds
( p . 1 = 0 iff p in VARS )
proof end;

Lm6: for a being object holds
( not a in SCI-unops or not a in SCI-binops )
proof end;

Lm7: for a being object holds
( not a in VARS or not a in SCI-ops )
proof end;

registration
cluster SCI-symbols -> non empty non trivial FinSequence-membered antichain-like ;
coherence
( not SCI-symbols is trivial & SCI-symbols is antichain-like )
proof end;
end;

definition
:: original: SCI-symbols
redefine func SCI-symbols -> non trivial Polish-language;
coherence
SCI-symbols is non trivial Polish-language ;
end;

definition
func SCI-op-arity -> Function of SCI-ops,NAT equals :: SUSZKO_1:def 12
(SCI-binops --> 2) +* (SCI-unops --> 1);
coherence
(SCI-binops --> 2) +* (SCI-unops --> 1) is Function of SCI-ops,NAT
proof end;
end;

:: deftheorem defines SCI-op-arity SUSZKO_1:def 12 :
SCI-op-arity = (SCI-binops --> 2) +* (SCI-unops --> 1);

Lm9: ( SCI-op-arity . 'not' = 1 & ( for a being object st a in SCI-binops holds
SCI-op-arity . a = 2 ) )
proof end;

definition
func SCI-arity -> Polish-arity-function of SCI-symbols equals :: SUSZKO_1:def 13
SCI-op-arity +* (VARS --> 0);
coherence
SCI-op-arity +* (VARS --> 0) is Polish-arity-function of SCI-symbols
proof end;
end;

:: deftheorem defines SCI-arity SUSZKO_1:def 13 :
SCI-arity = SCI-op-arity +* (VARS --> 0);

Lm10: for a being object st a in SCI-ops holds
SCI-arity . a = SCI-op-arity . a
proof end;

theorem Th6: :: SUSZKO_1:3
for a being object st a in VARS holds
SCI-arity . a = 0
proof end;

theorem Th7: :: SUSZKO_1:4
( SCI-arity . 'not' = 1 & ( for a being object st a in SCI-binops holds
SCI-arity . a = 2 ) )
proof end;

theorem Th9: :: SUSZKO_1:5
Polish-atoms (SCI-symbols,SCI-arity) = VARS
proof end;

definition
func SCI-formula-set -> full Polish-language of SCI-symbols equals :: SUSZKO_1:def 14
 Polish-WFF-set (SCI-symbols,SCI-arity);
coherence
Polish-WFF-set (SCI-symbols,SCI-arity) is full Polish-language of SCI-symbols ;
end;

:: deftheorem defines SCI-formula-set SUSZKO_1:def 14 :
SCI-formula-set = Polish-WFF-set (SCI-symbols,SCI-arity);

definition
mode SCI-formula is Polish-WFF of SCI-symbols,SCI-arity;
end;

registration
cluster non empty functional FinSequence-membered antichain-like for Element of bool SCI-formula-set;
existence
not for b1 being Subset of SCI-formula-set holds b1 is empty
proof end;
end;

definition
let n be Element of NAT ;
func x. n -> SCI-formula equals :: SUSZKO_1:def 15
<*0,n*>;
coherence
<*0,n*> is SCI-formula
proof end;
end;

:: deftheorem defines x. SUSZKO_1:def 15 :
for n being Element of NAT holds x. n = <*0,n*>;

theorem Th10: :: SUSZKO_1:6
for X being Extension of SCI-arity holds SCI-symbols c= dom X
proof end;

theorem Th7x: :: SUSZKO_1:7
for X being Extension of SCI-arity holds
( 'not' in dom X & X . 'not' = 1 & ( for a being object st a in SCI-binops holds
( a in dom X & X . a = 2 ) ) )
proof end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let n be Element of NAT ;
func x. (n,L) -> Formula of L equals :: SUSZKO_1:def 16
 x. n;
coherence
x. n is Formula of L
proof end;
end;

:: deftheorem defines x. SUSZKO_1:def 16 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for n being Element of NAT holds x. (n,L) = x. n;

theorem :: SUSZKO_1:8
for m, n being Element of NAT st m <> n holds
x. m <> x. n
proof end;

definition
let p be FinSequence;
func 'not' p -> FinSequence equals :: SUSZKO_1:def 17
'not' ^ p;
coherence
'not' ^ p is FinSequence ;
end;

:: deftheorem defines 'not' SUSZKO_1:def 17 :
for p being FinSequence holds 'not' p = 'not' ^ p;

definition
let p, q be FinSequence;
func p '&' q -> FinSequence equals :: SUSZKO_1:def 18
'&&s' ^ (p ^ q);
coherence
'&&s' ^ (p ^ q) is FinSequence ;
func p 'or' q -> FinSequence equals :: SUSZKO_1:def 19
'||s' ^ (p ^ q);
coherence
'||s' ^ (p ^ q) is FinSequence ;
func p '->' q -> FinSequence equals :: SUSZKO_1:def 20
'->' ^ (p ^ q);
coherence
'->' ^ (p ^ q) is FinSequence ;
func p '<->' q -> FinSequence equals :: SUSZKO_1:def 21
'<->' ^ (p ^ q);
coherence
'<->' ^ (p ^ q) is FinSequence ;
func p '==' q -> FinSequence equals :: SUSZKO_1:def 22
'==' ^ (p ^ q);
coherence
'==' ^ (p ^ q) is FinSequence ;
end;

:: deftheorem defines '&' SUSZKO_1:def 18 :
for p, q being FinSequence holds p '&' q = '&&s' ^ (p ^ q);

:: deftheorem defines 'or' SUSZKO_1:def 19 :
for p, q being FinSequence holds p 'or' q = '||s' ^ (p ^ q);

:: deftheorem defines '->' SUSZKO_1:def 20 :
for p, q being FinSequence holds p '->' q = '->' ^ (p ^ q);

:: deftheorem defines '<->' SUSZKO_1:def 21 :
for p, q being FinSequence holds p '<->' q = '<->' ^ (p ^ q);

:: deftheorem defines '==' SUSZKO_1:def 22 :
for p, q being FinSequence holds p '==' q = '==' ^ (p ^ q);

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
:: original: 'not'
redefine func 'not' t -> FinSequence equals :: SUSZKO_1:def 23
(Polish-unOp (X,L,'not')) . t;
compatibility
for b1 being FinSequence holds
( b1 = 'not' t iff b1 = (Polish-unOp (X,L,'not')) . t )
proof end;
let u be Formula of L;
:: original: '&'
redefine func t '&' u -> FinSequence equals :: SUSZKO_1:def 24
(Polish-binOp (X,L,'&&s')) . (t,u);
compatibility
for b1 being FinSequence holds
( b1 = t '&' u iff b1 = (Polish-binOp (X,L,'&&s')) . (t,u) )
proof end;
:: original: 'or'
redefine func t 'or' u -> FinSequence equals :: SUSZKO_1:def 25
(Polish-binOp (X,L,'||s')) . (t,u);
compatibility
for b1 being FinSequence holds
( b1 = t 'or' u iff b1 = (Polish-binOp (X,L,'||s')) . (t,u) )
proof end;
:: original: '->'
redefine func t '->' u -> FinSequence equals :: SUSZKO_1:def 26
(Polish-binOp (X,L,'->')) . (t,u);
compatibility
for b1 being FinSequence holds
( b1 = t '->' u iff b1 = (Polish-binOp (X,L,'->')) . (t,u) )
proof end;
:: original: '<->'
redefine func t '<->' u -> FinSequence equals :: SUSZKO_1:def 27
(Polish-binOp (X,L,'<->')) . (t,u);
compatibility
for b1 being FinSequence holds
( b1 = t '<->' u iff b1 = (Polish-binOp (X,L,'<->')) . (t,u) )
proof end;
:: original: '=='
redefine func t '==' u -> FinSequence equals :: SUSZKO_1:def 28
(Polish-binOp (X,L,'==')) . (t,u);
compatibility
for b1 being FinSequence holds
( b1 = t '==' u iff b1 = (Polish-binOp (X,L,'==')) . (t,u) )
proof end;
end;

:: deftheorem defines 'not' SUSZKO_1:def 23 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds 'not' t = (Polish-unOp (X,L,'not')) . t;

:: deftheorem defines '&' SUSZKO_1:def 24 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t, u being Formula of L holds t '&' u = (Polish-binOp (X,L,'&&s')) . (t,u);

:: deftheorem defines 'or' SUSZKO_1:def 25 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t, u being Formula of L holds t 'or' u = (Polish-binOp (X,L,'||s')) . (t,u);

:: deftheorem defines '->' SUSZKO_1:def 26 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t, u being Formula of L holds t '->' u = (Polish-binOp (X,L,'->')) . (t,u);

:: deftheorem defines '<->' SUSZKO_1:def 27 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t, u being Formula of L holds t '<->' u = (Polish-binOp (X,L,'<->')) . (t,u);

:: deftheorem defines '==' SUSZKO_1:def 28 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t, u being Formula of L holds t '==' u = (Polish-binOp (X,L,'==')) . (t,u);

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
:: original: 'not'
redefine func 'not' t -> Formula of L;
coherence
'not' t is Formula of L ;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t, u be Formula of L;
:: original: '&'
redefine func t '&' u -> Formula of L;
coherence
t '&' u is Formula of L ;
:: original: 'or'
redefine func t 'or' u -> Formula of L;
coherence
t 'or' u is Formula of L ;
:: original: '->'
redefine func t '->' u -> Formula of L;
coherence
t '->' u is Formula of L ;
:: original: '<->'
redefine func t '<->' u -> Formula of L;
coherence
t '<->' u is Formula of L ;
:: original: '=='
redefine func t '==' u -> Formula of L;
coherence
t '==' u is Formula of L ;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t, u be Formula of L;
func t => u -> Formula of L equals :: SUSZKO_1:def 29
t '==' (t '&' u);
coherence
t '==' (t '&' u) is Formula of L ;
end;

:: deftheorem defines => SUSZKO_1:def 29 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t, u being Formula of L holds t => u = t '==' (t '&' u);

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
let u be SCI-formula;
:: original: '->'
redefine func t '->' u -> Formula of L;
coherence
t '->' u is Formula of L
proof end;
:: original: '=='
redefine func t '==' u -> Formula of L;
coherence
t '==' u is Formula of L
proof end;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let u be SCI-formula;
let t be Formula of L;
:: original: '->'
redefine func u '->' t -> Formula of L;
coherence
u '->' t is Formula of L
proof end;
:: original: '=='
redefine func u '==' t -> Formula of L;
coherence
u '==' t is Formula of L
proof end;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
attr t is atomic means :: SUSZKO_1:def 30
t in Polish-atoms (SCI-symbols,SCI-arity);
attr t is negative means :: SUSZKO_1:def 31
 Polish-ext-head t = 'not' ;
attr t is conjunctive means :: SUSZKO_1:def 32
 Polish-ext-head t = '&&s' ;
attr t is disjunctive means :: SUSZKO_1:def 33
 Polish-ext-head t = '||s' ;
attr t is conditional means :: SUSZKO_1:def 34
 Polish-ext-head t = '->' ;
attr t is biconditional means :: SUSZKO_1:def 35
 Polish-ext-head t = '<->' ;
attr t is being_equality means :: SUSZKO_1:def 36
 Polish-ext-head t = '==' ;
end;

:: deftheorem defines atomic SUSZKO_1:def 30 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is atomic iff t in Polish-atoms (SCI-symbols,SCI-arity) );

:: deftheorem defines negative SUSZKO_1:def 31 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is negative iff Polish-ext-head t = 'not' );

:: deftheorem defines conjunctive SUSZKO_1:def 32 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is conjunctive iff Polish-ext-head t = '&&s' );

:: deftheorem defines disjunctive SUSZKO_1:def 33 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is disjunctive iff Polish-ext-head t = '||s' );

:: deftheorem defines conditional SUSZKO_1:def 34 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is conditional iff Polish-ext-head t = '->' );

:: deftheorem defines biconditional SUSZKO_1:def 35 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is biconditional iff Polish-ext-head t = '<->' );

:: deftheorem defines being_equality SUSZKO_1:def 36 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is being_equality iff Polish-ext-head t = '==' );

theorem :: SUSZKO_1:9
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is atomic iff t in VARS ) by Th9;

theorem :: SUSZKO_1:10
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is negative iff ex u being Formula of L st t = 'not' u )
proof end;

theorem :: SUSZKO_1:11
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for t being Formula of L holds
( t is conjunctive iff ex u, v being Formula of L st t = u '&' v )
proof end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
func SCI-prop-axioms L -> non empty Subset of L means :Def10p: :: SUSZKO_1:def 37
 for a being object holds
( a in it iff ex t, u, v being Formula of L st
( a = t '->' (u '->' t) or a = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or a = (('not' t) '->' ('not' u)) '->' (u '->' t) or a = (t '&' u) '->' ('not' (t '->' ('not' u))) or a = ('not' (t '->' ('not' u))) '->' (t '&' u) or a = (t 'or' u) '->' (('not' t) '->' u) or a = (('not' t) '->' u) '->' (t 'or' u) or a = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or a = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) ) );
existence
ex b1 being non empty Subset of L st
for a being object holds
( a in b1 iff ex t, u, v being Formula of L st
( a = t '->' (u '->' t) or a = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or a = (('not' t) '->' ('not' u)) '->' (u '->' t) or a = (t '&' u) '->' ('not' (t '->' ('not' u))) or a = ('not' (t '->' ('not' u))) '->' (t '&' u) or a = (t 'or' u) '->' (('not' t) '->' u) or a = (('not' t) '->' u) '->' (t 'or' u) or a = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or a = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) ) )
proof end;
uniqueness
for b1, b2 being non empty Subset of L st ( for a being object holds
( a in b1 iff ex t, u, v being Formula of L st
( a = t '->' (u '->' t) or a = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or a = (('not' t) '->' ('not' u)) '->' (u '->' t) or a = (t '&' u) '->' ('not' (t '->' ('not' u))) or a = ('not' (t '->' ('not' u))) '->' (t '&' u) or a = (t 'or' u) '->' (('not' t) '->' u) or a = (('not' t) '->' u) '->' (t 'or' u) or a = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or a = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) ) ) ) & ( for a being object holds
( a in b2 iff ex t, u, v being Formula of L st
( a = t '->' (u '->' t) or a = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or a = (('not' t) '->' ('not' u)) '->' (u '->' t) or a = (t '&' u) '->' ('not' (t '->' ('not' u))) or a = ('not' (t '->' ('not' u))) '->' (t '&' u) or a = (t 'or' u) '->' (('not' t) '->' u) or a = (('not' t) '->' u) '->' (t 'or' u) or a = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or a = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) ) ) ) holds
b1 = b2
proof end;
func SCI-id-axioms L -> non empty Subset of L means :Def10i: :: SUSZKO_1:def 38
 for a being object holds
( a in it iff ex t, u, v, w being Formula of L st
( a = t '==' t or a = (t '==' u) '->' (('not' t) '==' ('not' u)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or a = (t '==' u) '->' (t '->' u) ) );
existence
ex b1 being non empty Subset of L st
for a being object holds
( a in b1 iff ex t, u, v, w being Formula of L st
( a = t '==' t or a = (t '==' u) '->' (('not' t) '==' ('not' u)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or a = (t '==' u) '->' (t '->' u) ) )
proof end;
uniqueness
for b1, b2 being non empty Subset of L st ( for a being object holds
( a in b1 iff ex t, u, v, w being Formula of L st
( a = t '==' t or a = (t '==' u) '->' (('not' t) '==' ('not' u)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or a = (t '==' u) '->' (t '->' u) ) ) ) & ( for a being object holds
( a in b2 iff ex t, u, v, w being Formula of L st
( a = t '==' t or a = (t '==' u) '->' (('not' t) '==' ('not' u)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or a = (t '==' u) '->' (t '->' u) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10p defines SCI-prop-axioms SUSZKO_1:def 37 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for b3 being non empty Subset of L holds
( b3 = SCI-prop-axioms L iff for a being object holds
( a in b3 iff ex t, u, v being Formula of L st
( a = t '->' (u '->' t) or a = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or a = (('not' t) '->' ('not' u)) '->' (u '->' t) or a = (t '&' u) '->' ('not' (t '->' ('not' u))) or a = ('not' (t '->' ('not' u))) '->' (t '&' u) or a = (t 'or' u) '->' (('not' t) '->' u) or a = (('not' t) '->' u) '->' (t 'or' u) or a = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or a = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) ) ) );

:: deftheorem Def10i defines SCI-id-axioms SUSZKO_1:def 38 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for b3 being non empty Subset of L holds
( b3 = SCI-id-axioms L iff for a being object holds
( a in b3 iff ex t, u, v, w being Formula of L st
( a = t '==' t or a = (t '==' u) '->' (('not' t) '==' ('not' u)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or a = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or a = (t '==' u) '->' (t '->' u) ) ) );

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let B be Subset of L;
cluster non empty functional FinSequence-membered B -extending antichain-like for Element of bool L;
existence
ex b1 being non empty Subset of L st b1 is B -extending
proof end;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
func SCI-axioms L -> SCI-prop-axioms L -extending Subset of L equals :: SUSZKO_1:def 39
(SCI-prop-axioms L) \/ (SCI-id-axioms L);
coherence
(SCI-prop-axioms L) \/ (SCI-id-axioms L) is SCI-prop-axioms L -extending Subset of L
proof end;
end;

:: deftheorem defines SCI-axioms SUSZKO_1:def 39 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X holds SCI-axioms L = (SCI-prop-axioms L) \/ (SCI-id-axioms L);

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
func SCI-MP L -> Rule of L equals :: SUSZKO_1:def 40
 { [{t,(t '->' u)},u] where t, u is Formula of L : verum } ;
coherence
{ [{t,(t '->' u)},u] where t, u is Formula of L : verum } is Rule of L
proof end;
end;

:: deftheorem defines SCI-MP SUSZKO_1:def 40 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X holds SCI-MP L = { [{t,(t '->' u)},u] where t, u is Formula of L : verum } ;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
func SCI-rules L -> Rule of L equals :: SUSZKO_1:def 41
 SCI-MP L;
coherence
SCI-MP L is Rule of L ;
end;

:: deftheorem defines SCI-rules SUSZKO_1:def 41 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X holds SCI-rules L = SCI-MP L;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
mode Formula-sequence of L is FinSequence of L;
mode Formula-finset of L is finite Subset of L;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
:: original: {
redefine func {t} -> Formula-finset of L;
coherence
{t} is Formula-finset of L
proof end;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let B be Subset of L;
let a be object ;
attr a is B -provable means :Def60: :: SUSZKO_1:def 42
a is B, SCI-rules L -provable ;
end;

:: deftheorem Def60 defines -provable SUSZKO_1:def 42 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for B being Subset of L
for a being object holds
( a is B -provable iff a is B, SCI-rules L -provable );

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let B be Subset of L;
cluster B -axiomatic -> B -provable for object ;
coherence
for b1 being object st b1 is B -axiomatic holds
b1 is B -provable ;
end;

theorem Th20: :: SUSZKO_1:12
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for B being Subset of L
for t, u being Formula of L st t is B -provable & t '->' u is B -provable holds
u is B -provable
proof end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let a be object ;
attr a is L -prop-axiomatic means :: SUSZKO_1:def 43
a is SCI-prop-axioms L -axiomatic ;
attr a is L -id-axiomatic means :: SUSZKO_1:def 44
a is SCI-id-axioms L -axiomatic ;
attr a is L -SCI-axiomatic means :: SUSZKO_1:def 45
a is SCI-axioms L -axiomatic ;
attr a is L -SCI-provable means :: SUSZKO_1:def 46
a is SCI-axioms L -provable ;
end;

:: deftheorem defines -prop-axiomatic SUSZKO_1:def 43 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for a being object holds
( a is L -prop-axiomatic iff a is SCI-prop-axioms L -axiomatic );

:: deftheorem defines -id-axiomatic SUSZKO_1:def 44 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for a being object holds
( a is L -id-axiomatic iff a is SCI-id-axioms L -axiomatic );

:: deftheorem defines -SCI-axiomatic SUSZKO_1:def 45 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for a being object holds
( a is L -SCI-axiomatic iff a is SCI-axioms L -axiomatic );

:: deftheorem defines -SCI-provable SUSZKO_1:def 46 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for a being object holds
( a is L -SCI-provable iff a is SCI-axioms L -provable );

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
cluster -> L -prop-axiomatic for Element of SCI-prop-axioms L;
coherence
for b1 being Element of SCI-prop-axioms L holds b1 is L -prop-axiomatic by PROOFS_1:def 9;
cluster -> L -id-axiomatic for Element of SCI-id-axioms L;
coherence
for b1 being Element of SCI-id-axioms L holds b1 is L -id-axiomatic by PROOFS_1:def 9;
cluster -> L -SCI-axiomatic for Element of SCI-axioms L;
coherence
for b1 being Element of SCI-axioms L holds b1 is L -SCI-axiomatic by PROOFS_1:def 9;
cluster L -SCI-axiomatic -> L -SCI-provable for object ;
coherence
for b1 being object st b1 is L -SCI-axiomatic holds
b1 is L -SCI-provable ;
cluster L -prop-axiomatic -> L -SCI-axiomatic for object ;
coherence
for b1 being object st b1 is L -prop-axiomatic holds
b1 is L -SCI-axiomatic ;
cluster L -id-axiomatic -> L -SCI-axiomatic for object ;
coherence
for b1 being object st b1 is L -id-axiomatic holds
b1 is L -SCI-axiomatic
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
cluster t '==' t -> L -id-axiomatic ;
coherence
t '==' t is L -id-axiomatic
proof end;
let u be Formula of L;
cluster t '->' (u '->' t) -> L -prop-axiomatic ;
coherence
t '->' (u '->' t) is L -prop-axiomatic
proof end;
cluster (('not' t) '->' ('not' u)) '->' (u '->' t) -> L -prop-axiomatic ;
coherence
(('not' t) '->' ('not' u)) '->' (u '->' t) is L -prop-axiomatic
proof end;
cluster (t '&' u) '->' ('not' (t '->' ('not' u))) -> L -prop-axiomatic ;
coherence
(t '&' u) '->' ('not' (t '->' ('not' u))) is L -prop-axiomatic
proof end;
cluster ('not' (t '->' ('not' u))) '->' (t '&' u) -> L -prop-axiomatic ;
coherence
('not' (t '->' ('not' u))) '->' (t '&' u) is L -prop-axiomatic
proof end;
cluster (t 'or' u) '->' (('not' t) '->' u) -> L -prop-axiomatic ;
coherence
(t 'or' u) '->' (('not' t) '->' u) is L -prop-axiomatic
proof end;
cluster (('not' t) '->' u) '->' (t 'or' u) -> L -prop-axiomatic ;
coherence
(('not' t) '->' u) '->' (t 'or' u) is L -prop-axiomatic
proof end;
cluster (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) -> L -prop-axiomatic ;
coherence
(t '<->' u) '->' ((t '->' u) '&' (u '->' t)) is L -prop-axiomatic
proof end;
cluster ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) -> L -prop-axiomatic ;
coherence
((t '->' u) '&' (u '->' t)) '->' (t '<->' u) is L -prop-axiomatic
proof end;
cluster (t '==' u) '->' (('not' t) '==' ('not' u)) -> L -id-axiomatic ;
coherence
(t '==' u) '->' (('not' t) '==' ('not' u)) is L -id-axiomatic
proof end;
cluster (t '==' u) '->' (t '->' u) -> L -id-axiomatic ;
coherence
(t '==' u) '->' (t '->' u) is L -id-axiomatic
proof end;
let v be Formula of L;
cluster (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) -> L -prop-axiomatic ;
coherence
(t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) is L -prop-axiomatic
proof end;
let w be Formula of L;
let O be Element of SCI-binops ;
cluster ((t '==' u) '&' (v '==' w)) '->' (((Polish-binOp (X,L,O)) . (t,v)) '==' ((Polish-binOp (X,L,O)) . (u,w))) -> L -id-axiomatic ;
coherence
((t '==' u) '&' (v '==' w)) '->' (((Polish-binOp (X,L,O)) . (t,v)) '==' ((Polish-binOp (X,L,O)) . (u,w))) is L -id-axiomatic
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like L -prop-axiomatic for Element of L;
existence
ex b1 being Formula of L st b1 is L -prop-axiomatic
proof end;
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like L -id-axiomatic for Element of L;
existence
ex b1 being Formula of L st b1 is L -id-axiomatic
proof end;
end;

Lm20: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t being Formula of L st t is L -prop-axiomatic holds
t is C -provable
;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
cluster L -prop-axiomatic -> SCI-prop-axioms L -provable for Element of L;
coherence
for b1 being Formula of L st b1 is L -prop-axiomatic holds
b1 is SCI-prop-axioms L -provable ;
let C be SCI-prop-axioms L -extending Subset of L;
cluster non C -provable -> non SCI-prop-axioms L -provable for Element of L;
coherence
for b1 being Formula of L st not b1 is C -provable holds
not b1 is SCI-prop-axioms L -provable ;
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like C -provable for Element of L;
existence
ex b1 being Formula of L st b1 is C -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t be Formula of L;
let u be C -provable Formula of L;
cluster t '->' u -> C -provable ;
coherence
t '->' u is C -provable
proof end;
end;

Lm21: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L st u '->' v is C -provable holds
(t '->' u) '->' (t '->' v) is C -provable
proof end;

theorem Th21: :: SUSZKO_1:13
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L st t '->' u is C -provable & u '->' v is C -provable holds
t '->' v is C -provable
proof end;

theorem Th22: :: SUSZKO_1:14
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t being Formula of L holds t '->' t is C -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
cluster t '->' t -> SCI-prop-axioms L -provable ;
coherence
t '->' t is SCI-prop-axioms L -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t be C -provable Formula of L;
let u be Formula of L;
cluster (t '->' u) '->' u -> C -provable ;
coherence
(t '->' u) '->' u is C -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t be Formula of L;
let u be C -provable Formula of L;
let v be Formula of L;
cluster (t '->' (u '->' v)) '->' (t '->' v) -> C -provable ;
coherence
(t '->' (u '->' v)) '->' (t '->' v) is C -provable
proof end;
end;

Lm23: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds (t '->' (t '->' u)) '->' (t '->' u) is C -provable
proof end;

theorem Th23: :: SUSZKO_1:15
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L st t '->' (t '->' u) is C -provable holds
t '->' u is C -provable
proof end;

theorem Th24: :: SUSZKO_1:16
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L st t '->' (u '->' v) is C -provable holds
u '->' (t '->' v) is C -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t, u be Formula of L;
cluster (t '->' (t '->' u)) '->' (t '->' u) -> SCI-prop-axioms L -provable ;
coherence
(t '->' (t '->' u)) '->' (t '->' u) is SCI-prop-axioms L -provable
proof end;
end;

Lm24: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L st ('not' t) '->' ('not' u) is C -provable holds
u '->' t is C -provable
proof end;

Lm25: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L st t '->' (('not' u) '->' ('not' v)) is C -provable holds
t '->' (v '->' u) is C -provable
proof end;

theorem Th26: :: SUSZKO_1:17
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t being Formula of L holds ('not' ('not' t)) '->' t is C -provable
proof end;

theorem Th27: :: SUSZKO_1:18
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t being Formula of L holds t '->' ('not' ('not' t)) is C -provable
proof end;

Lm26: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L st t '->' u is C -provable holds
(u '->' v) '->' (t '->' v) is C -provable
proof end;

Lm27: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds (t '->' u) '->' (('not' u) '->' ('not' t)) is C -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
cluster ('not' ('not' t)) '->' t -> SCI-prop-axioms L -provable ;
coherence
('not' ('not' t)) '->' t is SCI-prop-axioms L -provable
proof end;
cluster t '->' ('not' ('not' t)) -> SCI-prop-axioms L -provable ;
coherence
t '->' ('not' ('not' t)) is SCI-prop-axioms L -provable
proof end;
let u be Formula of L;
cluster (t '->' u) '->' (('not' u) '->' ('not' t)) -> SCI-prop-axioms L -provable ;
coherence
(t '->' u) '->' (('not' u) '->' ('not' t)) is SCI-prop-axioms L -provable
proof end;
end;

theorem Th28: :: SUSZKO_1:19
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L st ('not' t) '->' u is C -provable holds
('not' u) '->' t is C -provable
proof end;

theorem :: SUSZKO_1:20
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L st t '->' ('not' u) is C -provable holds
u '->' ('not' t) is C -provable
proof end;

theorem Th30: :: SUSZKO_1:21
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( ('not' t) '->' ('not' u) is C -provable iff u '->' t is C -provable )
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t be Formula of L;
let u be C -provable Formula of L;
cluster ('not' u) '->' t -> C -provable ;
coherence
('not' u) '->' t is C -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
cluster t '->' t -> L -SCI-provable ;
coherence
t '->' t is L -SCI-provable ;
cluster t '->' ('not' ('not' t)) -> L -SCI-provable ;
coherence
t '->' ('not' ('not' t)) is L -SCI-provable ;
cluster ('not' ('not' t)) '->' t -> L -SCI-provable ;
coherence
('not' ('not' t)) '->' t is L -SCI-provable ;
let u be L -SCI-provable Formula of L;
cluster t '->' u -> L -SCI-provable ;
coherence
t '->' u is L -SCI-provable
proof end;
end;

theorem Th32: :: SUSZKO_1:22
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds ('not' t) '->' (t '->' u) is C -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t, u be Formula of L;
cluster ('not' t) '->' (t '->' u) -> SCI-prop-axioms L -provable ;
coherence
('not' t) '->' (t '->' u) is SCI-prop-axioms L -provable
proof end;
cluster t '->' (('not' t) '->' u) -> SCI-prop-axioms L -provable ;
coherence
t '->' (('not' t) '->' u) is SCI-prop-axioms L -provable
proof end;
end;

theorem :: SUSZKO_1:23
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L st 'not' t is C -provable holds
t '->' u is C -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t, u be Formula of L;
cluster t '->' ((t '->' u) '->' u) -> SCI-prop-axioms L -provable ;
coherence
t '->' ((t '->' u) '->' u) is SCI-prop-axioms L -provable
proof end;
end;

theorem Th36: :: SUSZKO_1:24
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L holds
( t '->' (u '->' v) is C -provable iff t '->' (('not' v) '->' ('not' u)) is C -provable )
proof end;

theorem Th40: :: SUSZKO_1:25
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( (t '&' u) '->' t is C -provable & (t '&' u) '->' u is C -provable )
proof end;

theorem Th41: :: SUSZKO_1:26
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds t '->' (u '->' (t '&' u)) is C -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t, u be Formula of L;
cluster (t '&' u) '->' t -> SCI-prop-axioms L -provable ;
coherence
(t '&' u) '->' t is SCI-prop-axioms L -provable
proof end;
cluster (t '&' u) '->' u -> SCI-prop-axioms L -provable ;
coherence
(t '&' u) '->' u is SCI-prop-axioms L -provable
proof end;
cluster t '->' (u '->' (t '&' u)) -> SCI-prop-axioms L -provable ;
coherence
t '->' (u '->' (t '&' u)) is SCI-prop-axioms L -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t be Formula of L;
let u be C -provable Formula of L;
cluster t '->' (t '&' u) -> C -provable ;
coherence
t '->' (t '&' u) is C -provable
proof end;
cluster t '->' (u '&' t) -> C -provable ;
coherence
t '->' (u '&' t) is C -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t, u be C -provable Formula of L;
cluster t '&' u -> C -provable ;
coherence
t '&' u is C -provable
proof end;
end;

theorem :: SUSZKO_1:27
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L holds
( (t '&' u) '->' v is C -provable iff t '->' (u '->' v) is C -provable )
proof end;

theorem Th43: :: SUSZKO_1:28
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( t '&' u is C -provable iff ( t is C -provable & u is C -provable ) )
proof end;

theorem Th44: :: SUSZKO_1:29
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L holds
( t '->' (u '&' v) is C -provable iff ( t '->' u is C -provable & t '->' v is C -provable ) )
proof end;

theorem Th45: :: SUSZKO_1:30
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( t '->' (t 'or' u) is C -provable & u '->' (t 'or' u) is C -provable )
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let t be Formula of L;
cluster t 'or' ('not' t) -> SCI-prop-axioms L -provable ;
coherence
t 'or' ('not' t) is SCI-prop-axioms L -provable
proof end;
let u be Formula of L;
cluster t '->' (t 'or' u) -> SCI-prop-axioms L -provable ;
coherence
t '->' (t 'or' u) is SCI-prop-axioms L -provable
proof end;
cluster u '->' (t 'or' u) -> SCI-prop-axioms L -provable ;
coherence
u '->' (t 'or' u) is SCI-prop-axioms L -provable
proof end;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let C be SCI-prop-axioms L -extending Subset of L;
let t be C -provable Formula of L;
let u be Formula of L;
cluster t 'or' u -> C -provable ;
coherence
t 'or' u is C -provable
proof end;
cluster u 'or' t -> C -provable ;
coherence
u 'or' t is C -provable
proof end;
end;

theorem Th46: :: SUSZKO_1:31
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t being Formula of L holds (('not' t) '->' t) '->' t is C -provable
proof end;

theorem Th47: :: SUSZKO_1:32
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v being Formula of L holds
( (t 'or' u) '->' v is C -provable iff ( t '->' v is C -provable & u '->' v is C -provable ) )
proof end;

theorem :: SUSZKO_1:33
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u, v, w being Formula of L st t '->' v is C -provable & u '->' w is C -provable holds
( (t 'or' u) '->' (v 'or' w) is C -provable & (t '&' u) '->' (v '&' w) is C -provable )
proof end;

Lm50: for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L st u is C \/ {t} -provable holds
t '->' u is C -provable
proof end;

theorem :: SUSZKO_1:34
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for C being SCI-prop-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( t '->' u is C -provable iff u is C \/ {t} -provable )
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
cluster non D -provable -> non L -SCI-provable for Element of L;
coherence
for b1 being Formula of L st not b1 is D -provable holds
not b1 is L -SCI-provable by Def60;
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like D -provable for Element of L;
existence
ex b1 being Formula of L st b1 is D -provable
proof end;
end;

theorem Th60: :: SUSZKO_1:35
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L st t '==' u is D -provable holds
t '->' u is D -provable
proof end;

theorem Th61: :: SUSZKO_1:36
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L st t '==' u is D -provable holds
('not' t) '==' ('not' u) is D -provable
proof end;

theorem Th62: :: SUSZKO_1:37
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L holds (t '==' u) '->' (u '==' t) is D -provable
proof end;

theorem Th63: :: SUSZKO_1:38
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L st t '==' u is D -provable holds
u '==' t is D -provable
proof end;

theorem :: SUSZKO_1:39
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u, v being Formula of L holds ((t '==' u) '&' (v '==' u)) '->' (t '==' v) is D -provable
proof end;

theorem :: SUSZKO_1:40
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L st t is D -provable & t => u is D -provable holds
u is D -provable
proof end;

theorem Th66: :: SUSZKO_1:41
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u, v, w being Formula of L st t '==' u is D -provable & v '==' w is D -provable holds
( (t '&' v) '==' (u '&' w) is D -provable & (t '&' v) '->' (u '&' w) is D -provable & ( t '&' v is D -provable implies u '&' w is D -provable ) & (t 'or' v) '==' (u 'or' w) is D -provable & (t 'or' v) '->' (u 'or' w) is D -provable & ( t 'or' v is D -provable implies u 'or' w is D -provable ) & (t '->' v) '==' (u '->' w) is D -provable & (t '->' v) '->' (u '->' w) is D -provable & ( t '->' v is D -provable implies u '->' w is D -provable ) & (t '<->' v) '==' (u '<->' w) is D -provable & (t '<->' v) '->' (u '<->' w) is D -provable & ( t '<->' v is D -provable implies u '<->' w is D -provable ) & (t '==' v) '==' (u '==' w) is D -provable & (t '==' v) '->' (u '==' w) is D -provable & ( t '==' v is D -provable implies u '==' w is D -provable ) & (t => v) '==' (u => w) is D -provable & (t => v) '->' (u => w) is D -provable & ( t => v is D -provable implies u => w is D -provable ) )
proof end;

theorem Th67: :: SUSZKO_1:42
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u, v being Formula of L holds
( (t '==' u) '->' ((t '&' v) '==' (u '&' v)) is D -provable & (t '==' u) '->' ((v '&' t) '==' (v '&' u)) is D -provable & (t '==' u) '->' ((t 'or' v) '==' (u 'or' v)) is D -provable & (t '==' u) '->' ((v 'or' t) '==' (v 'or' u)) is D -provable & (t '==' u) '->' ((t '->' v) '==' (u '->' v)) is D -provable & (t '==' u) '->' ((v '->' t) '==' (v '->' u)) is D -provable & (t '==' u) '->' ((t '<->' v) '==' (u '<->' v)) is D -provable & (t '==' u) '->' ((v '<->' t) '==' (v '<->' u)) is D -provable & (t '==' u) '->' ((t '==' v) '==' (u '==' v)) is D -provable & (t '==' u) '->' ((v '==' t) '==' (v '==' u)) is D -provable & (t '==' u) '->' ((t => v) '==' (u => v)) is D -provable & (t '==' u) '->' ((v => t) '==' (v => u)) is D -provable )
proof end;

theorem Th68: :: SUSZKO_1:43
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u, v being Formula of L st t '==' u is D -provable holds
( ( t is D -provable implies u is D -provable ) & ( u is D -provable implies t is D -provable ) & (t '&' v) '==' (u '&' v) is D -provable & (t '&' v) '->' (u '&' v) is D -provable & ( t '&' v is D -provable implies u '&' v is D -provable ) & (v '&' t) '==' (v '&' u) is D -provable & (v '&' t) '->' (v '&' u) is D -provable & ( v '&' t is D -provable implies v '&' u is D -provable ) & (t 'or' v) '==' (u 'or' v) is D -provable & (t 'or' v) '->' (u 'or' v) is D -provable & ( t 'or' v is D -provable implies u 'or' v is D -provable ) & (v 'or' t) '==' (v 'or' u) is D -provable & (v 'or' t) '->' (v 'or' u) is D -provable & ( v 'or' t is D -provable implies v 'or' u is D -provable ) & (t '->' v) '==' (u '->' v) is D -provable & (t '->' v) '->' (u '->' v) is D -provable & ( t '->' v is D -provable implies u '->' v is D -provable ) & (v '->' t) '==' (v '->' u) is D -provable & (v '->' t) '->' (v '->' u) is D -provable & ( v '->' t is D -provable implies v '->' u is D -provable ) & (t '<->' v) '==' (u '<->' v) is D -provable & (t '<->' v) '->' (u '<->' v) is D -provable & ( t '<->' v is D -provable implies u '<->' v is D -provable ) & (v '<->' t) '==' (v '<->' u) is D -provable & (v '<->' t) '->' (v '<->' u) is D -provable & ( v '<->' t is D -provable implies v '<->' u is D -provable ) & (t '==' v) '==' (u '==' v) is D -provable & (t '==' v) '->' (u '==' v) is D -provable & ( t '==' v is D -provable implies u '==' v is D -provable ) & (v '==' t) '==' (v '==' u) is D -provable & (v '==' t) '->' (v '==' u) is D -provable & ( v '==' t is D -provable implies v '==' u is D -provable ) & (t => v) '==' (u => v) is D -provable & (t => v) '->' (u => v) is D -provable & ( t => v is D -provable implies u => v is D -provable ) & (v => t) '==' (v => u) is D -provable & (v => t) '->' (v => u) is D -provable & ( v => t is D -provable implies v => u is D -provable ) )
proof end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
mode Congruence of L -> Equivalence_Relation of L means :Def100: :: SUSZKO_1:def 47
 for t, u, v, w being Formula of L st [t,u] in it & [v,w] in it holds
( [('not' t),('not' u)] in it & [(t '&' v),(u '&' w)] in it & [(t 'or' v),(u 'or' w)] in it & [(t '->' v),(u '->' w)] in it & [(t '<->' v),(u '<->' w)] in it & [(t '==' v),(u '==' w)] in it );
existence
ex b1 being Equivalence_Relation of L st
for t, u, v, w being Formula of L st [t,u] in b1 & [v,w] in b1 holds
( [('not' t),('not' u)] in b1 & [(t '&' v),(u '&' w)] in b1 & [(t 'or' v),(u 'or' w)] in b1 & [(t '->' v),(u '->' w)] in b1 & [(t '<->' v),(u '<->' w)] in b1 & [(t '==' v),(u '==' w)] in b1 )
proof end;
end;

:: deftheorem Def100 defines Congruence SUSZKO_1:def 47 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for b3 being Equivalence_Relation of L holds
( b3 is Congruence of L iff for t, u, v, w being Formula of L st [t,u] in b3 & [v,w] in b3 holds
( [('not' t),('not' u)] in b3 & [(t '&' v),(u '&' w)] in b3 & [(t 'or' v),(u 'or' w)] in b3 & [(t '->' v),(u '->' w)] in b3 & [(t '<->' v),(u '<->' w)] in b3 & [(t '==' v),(u '==' w)] in b3 ) );

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
cluster non empty for Element of bool (bool L);
existence
not for b1 being Subset-Family of L holds b1 is empty
proof end;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let E be Congruence of L;
mode Equivalence_Class of E is Element of Class E;
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let E be Congruence of L;
let t be Formula of L;
func E -class t -> Equivalence_Class of E equals :: SUSZKO_1:def 48
 Class (E,t);
coherence
Class (E,t) is Equivalence_Class of E by EQREL_1:def 3;
end;

:: deftheorem defines -class SUSZKO_1:def 48 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for t being Formula of L holds E -class t = Class (E,t);

theorem Th70: :: SUSZKO_1:44
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for t, u being Formula of L holds
( [t,u] in E iff E -class t = E -class u )
proof end;

theorem Th71: :: SUSZKO_1:45
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d being Equivalence_Class of E ex t being Formula of L st d = E -class t
proof end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let E be Congruence of L;
let d be Equivalence_Class of E;
func 'not' d -> Equivalence_Class of E means :Def101: :: SUSZKO_1:def 49
 ex t being Formula of L st
( d = E -class t & it = E -class ('not' t) );
existence
ex b1 being Equivalence_Class of E ex t being Formula of L st
( d = E -class t & b1 = E -class ('not' t) )
proof end;
uniqueness
for b1, b2 being Equivalence_Class of E st ex t being Formula of L st
( d = E -class t & b1 = E -class ('not' t) ) & ex t being Formula of L st
( d = E -class t & b2 = E -class ('not' t) ) holds
b1 = b2
proof end;
let e be Equivalence_Class of E;
func d '&' e -> Equivalence_Class of E means :Def102: :: SUSZKO_1:def 50
 ex t, u being Formula of L st
( d = E -class t & e = E -class u & it = E -class (t '&' u) );
existence
ex b1 being Equivalence_Class of E ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '&' u) )
proof end;
uniqueness
for b1, b2 being Equivalence_Class of E st ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '&' u) ) & ex t, u being Formula of L st
( d = E -class t & e = E -class u & b2 = E -class (t '&' u) ) holds
b1 = b2
proof end;
func d 'or' e -> Equivalence_Class of E means :Def103: :: SUSZKO_1:def 51
 ex t, u being Formula of L st
( d = E -class t & e = E -class u & it = E -class (t 'or' u) );
existence
ex b1 being Equivalence_Class of E ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t 'or' u) )
proof end;
uniqueness
for b1, b2 being Equivalence_Class of E st ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t 'or' u) ) & ex t, u being Formula of L st
( d = E -class t & e = E -class u & b2 = E -class (t 'or' u) ) holds
b1 = b2
proof end;
func d '->' e -> Equivalence_Class of E means :Def104: :: SUSZKO_1:def 52
 ex t, u being Formula of L st
( d = E -class t & e = E -class u & it = E -class (t '->' u) );
existence
ex b1 being Equivalence_Class of E ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '->' u) )
proof end;
uniqueness
for b1, b2 being Equivalence_Class of E st ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '->' u) ) & ex t, u being Formula of L st
( d = E -class t & e = E -class u & b2 = E -class (t '->' u) ) holds
b1 = b2
proof end;
func d '<->' e -> Equivalence_Class of E means :Def105: :: SUSZKO_1:def 53
 ex t, u being Formula of L st
( d = E -class t & e = E -class u & it = E -class (t '<->' u) );
existence
ex b1 being Equivalence_Class of E ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '<->' u) )
proof end;
uniqueness
for b1, b2 being Equivalence_Class of E st ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '<->' u) ) & ex t, u being Formula of L st
( d = E -class t & e = E -class u & b2 = E -class (t '<->' u) ) holds
b1 = b2
proof end;
func d '==' e -> Equivalence_Class of E means :Def106: :: SUSZKO_1:def 54
 ex t, u being Formula of L st
( d = E -class t & e = E -class u & it = E -class (t '==' u) );
existence
ex b1 being Equivalence_Class of E ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '==' u) )
proof end;
uniqueness
for b1, b2 being Equivalence_Class of E st ex t, u being Formula of L st
( d = E -class t & e = E -class u & b1 = E -class (t '==' u) ) & ex t, u being Formula of L st
( d = E -class t & e = E -class u & b2 = E -class (t '==' u) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def101 defines 'not' SUSZKO_1:def 49 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d, b5 being Equivalence_Class of E holds
( b5 = 'not' d iff ex t being Formula of L st
( d = E -class t & b5 = E -class ('not' t) ) );

:: deftheorem Def102 defines '&' SUSZKO_1:def 50 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d, e, b6 being Equivalence_Class of E holds
( b6 = d '&' e iff ex t, u being Formula of L st
( d = E -class t & e = E -class u & b6 = E -class (t '&' u) ) );

:: deftheorem Def103 defines 'or' SUSZKO_1:def 51 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d, e, b6 being Equivalence_Class of E holds
( b6 = d 'or' e iff ex t, u being Formula of L st
( d = E -class t & e = E -class u & b6 = E -class (t 'or' u) ) );

:: deftheorem Def104 defines '->' SUSZKO_1:def 52 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d, e, b6 being Equivalence_Class of E holds
( b6 = d '->' e iff ex t, u being Formula of L st
( d = E -class t & e = E -class u & b6 = E -class (t '->' u) ) );

:: deftheorem Def105 defines '<->' SUSZKO_1:def 53 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d, e, b6 being Equivalence_Class of E holds
( b6 = d '<->' e iff ex t, u being Formula of L st
( d = E -class t & e = E -class u & b6 = E -class (t '<->' u) ) );

:: deftheorem Def106 defines '==' SUSZKO_1:def 54 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for E being Congruence of L
for d, e, b6 being Equivalence_Class of E holds
( b6 = d '==' e iff ex t, u being Formula of L st
( d = E -class t & e = E -class u & b6 = E -class (t '==' u) ) );

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
func EqRel D -> Congruence of L means :Def110: :: SUSZKO_1:def 55
 for t, u being Formula of L holds
( [t,u] in it iff t '==' u is D -provable );
existence
ex b1 being Congruence of L st
for t, u being Formula of L holds
( [t,u] in b1 iff t '==' u is D -provable )
proof end;
uniqueness
for b1, b2 being Congruence of L st ( for t, u being Formula of L holds
( [t,u] in b1 iff t '==' u is D -provable ) ) & ( for t, u being Formula of L holds
( [t,u] in b2 iff t '==' u is D -provable ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def110 defines EqRel SUSZKO_1:def 55 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for b4 being Congruence of L holds
( b4 = EqRel D iff for t, u being Formula of L holds
( [t,u] in b4 iff t '==' u is D -provable ) );

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
mode Equivalence_Class of D is Equivalence_Class of (EqRel D);
end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
let t be Formula of L;
func D -class t -> Equivalence_Class of D equals :: SUSZKO_1:def 56
(EqRel D) -class t;
coherence
(EqRel D) -class t is Equivalence_Class of D ;
end;

:: deftheorem defines -class SUSZKO_1:def 56 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t being Formula of L holds D -class t = (EqRel D) -class t;

theorem Th80: :: SUSZKO_1:46
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( t '==' u is D -provable iff D -class t = D -class u )
proof end;

theorem Th81: :: SUSZKO_1:47
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for x being Equivalence_Class of D ex t being Formula of L st x = D -class t
proof end;

definition
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
let x be Equivalence_Class of D;
attr x is D -provable means :: SUSZKO_1:def 57
 ex t being Formula of L st
( x = D -class t & t is D -provable );
end;

:: deftheorem defines -provable SUSZKO_1:def 57 :
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for x being Equivalence_Class of D holds
( x is D -provable iff ex t being Formula of L st
( x = D -class t & t is D -provable ) );

theorem :: SUSZKO_1:48
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for x, y being Equivalence_Class of D holds
( y = 'not' x iff ex t being Formula of L st
( x = D -class t & y = D -class ('not' t) ) )
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
let t be D -provable Formula of L;
cluster D -class t -> D -provable ;
coherence
D -class t is D -provable ;
end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
cluster zero D -provable for Element of Class (EqRel D);
existence
ex b1 being Equivalence_Class of D st b1 is D -provable
proof end;
end;

theorem Th90: :: SUSZKO_1:49
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t being Formula of L st D -class t is D -provable holds
t is D -provable
proof end;

registration
let X be Extension of SCI-arity ;
let L be Polish-ext-set of X;
let D be SCI-axioms L -extending Subset of L;
let x be D -provable Equivalence_Class of D;
cluster -> D -provable for Element of x;
coherence
for b1 being Element of x holds b1 is D -provable
proof end;
end;

theorem :: SUSZKO_1:50
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for x, y being Equivalence_Class of D holds
( x '&' y is D -provable iff ( x is D -provable & y is D -provable ) )
proof end;

theorem :: SUSZKO_1:51
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for x, y being Equivalence_Class of D holds
( x '==' y is D -provable iff x = y )
proof end;

theorem :: SUSZKO_1:52
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( D -class ('not' t) = 'not' (D -class t) & D -class (t '&' u) = (D -class t) '&' (D -class u) & D -class (t 'or' u) = (D -class t) 'or' (D -class u) & D -class (t '->' u) = (D -class t) '->' (D -class u) & D -class (t '<->' u) = (D -class t) '<->' (D -class u) & D -class (t '==' u) = (D -class t) '==' (D -class u) ) by Def101, Def102, Def103, Def104, Def105, Def106;

theorem :: SUSZKO_1:53
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for x, y being Equivalence_Class of D st x is D -provable holds
( x 'or' y is D -provable & y 'or' x is D -provable )
proof end;

theorem Th96: :: SUSZKO_1:54
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L holds
( t '<->' u is D -provable iff ( t '->' u is D -provable & u '->' t is D -provable ) )
proof end;

theorem :: SUSZKO_1:55
for X being Extension of SCI-arity
for L being Polish-ext-set of X
for D being SCI-axioms b2 -extending Subset of L
for t, u being Formula of L st t '<->' u is D -provable holds
u '<->' t is D -provable
proof end;