for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for A being ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) st ex m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st succ m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & rng f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( finite ) Element of bool b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty finite V43() ) set ) ) = A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & ( for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( finite ) Element of bool b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty finite V43() ) set ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( finite ) Element of bool b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty finite V43() ) set ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) in f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) . (union n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal ) set ) : ( ( ) ( ) set ) = union (rng f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -defined b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like quasi_total finite ) Function of b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( finite ) Element of bool b₂ : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty finite V43() ) set ) ) : ( ( ) ( ) set ) ;

for A being ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
( union A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ) set ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & ( for a being ( ( ) ( ) set ) holds
( not a : ( ( ) ( ) set ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) or a : ( ( ) ( ) set ) in union A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ) set ) or a : ( ( ) ( ) set ) = union A : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,C : ( ( non empty ) ( non empty ) set ) )
for X being ( ( finite ) ( finite ) set ) st ( for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) c= f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & X : ( ( finite ) ( finite ) set ) c= union (rng f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( finite ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
ex k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( finite ) ( finite ) set ) c= f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let p be ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
antonym Inconsistent X for Consistent ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let f be ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
antonym Inconsistent f for Consistent ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for g being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is Consistent & rng g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( finite ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is Consistent ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for f, g being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st |- f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty trivial Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
|- (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty trivial Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is Inconsistent iff for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is Inconsistent holds
ex Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st
( Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite & Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is Inconsistent ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p, q being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ {p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex g being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st
( rng g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( finite ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & |- (g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty trivial Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*q : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty trivial Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ {('not' p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is Inconsistent ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- 'not' p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ {p : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is Inconsistent ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for f being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st ( for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is Consistent & f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) c= f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) holds
union (rng f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) Element of bool (bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is Consistent ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for A being ( ( non empty ) ( non empty ) set ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is Inconsistent holds
for J being ( ( ) ( Relation-like QC-pred_symbols b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) -defined relations_on b₃ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) interpretation of Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) )
for v being ( ( ) ( Relation-like bound_QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Valuations_in (Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of bound_QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) ) holds not J : ( ( ) ( Relation-like QC-pred_symbols b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) -defined relations_on b₃ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) interpretation of b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Valuations_in (b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of bound_QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-variables b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) ) |= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

for Al being ( ( ) ( non empty Relation-like ) QC-alphabet ) holds {(VERUM Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( ) Element of CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) Element of bool (CQC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b₁ : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is Consistent ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let P be ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) ) ;
let ll be ( ( bound_QC-variables Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-variables Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued the_arity_of P : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined QC-variables Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) -valued bound_QC-variables Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-variables Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite the_arity_of P : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) CQC-variable_list of the_arity_of P : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) , ( ( ) ( non empty ) set ) ) ;
:: original: !
redefine func P ! ll -> ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( non empty Relation-like ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

let Al be ( ( ) ( non empty Relation-like ) QC-alphabet ) ;
let CX be ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ;