:: KURATO_1 semantic presentation

begin

notation
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
synonym A - for Cl A;
end;

theorem :: KURATO_1:1
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds ((((((A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = ((A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
func Kurat14Part A -> ( ( ) ( ) set ) equals :: KURATO_1:def 1
{A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((((A : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Kurat14Part A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -> finite ;
end;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
func Kurat14Set A -> ( ( ) ( ) Subset-Family of ) equals :: KURATO_1:def 2
{A : ( ( non empty ) ( non empty ) set ) ,(A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) \/ {(A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) : ( ( ) ( non empty finite ) set ) ;
end;

theorem :: KURATO_1:2
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) = (Kurat14Part A : ( ( ) ( ) Subset of ) ) : ( ( ) ( finite ) set ) \/ (Kurat14Part (A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( finite ) set ) : ( ( ) ( finite ) set ) ;

theorem :: KURATO_1:3
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & A : ( ( ) ( ) Subset of ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & (A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & ((A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & (((A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & ((((A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & (((((A : ( ( ) ( ) Subset of ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) ) ;

theorem :: KURATO_1:4
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & (A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & ((A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & (((A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & ((((A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & (((((A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & ((((((A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) ) ;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
func Kurat14ClPart A -> ( ( ) ( ) Subset-Family of ) equals :: KURATO_1:def 3
{(A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) ;
func Kurat14OpPart A -> ( ( ) ( ) Subset-Family of ) equals :: KURATO_1:def 4
{((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,((((((A : ( ( non empty ) ( non empty ) set ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(((((((A : ( ( non empty ) ( non empty ) set ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) ;
end;

theorem :: KURATO_1:5
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) = ({A : ( ( ) ( ) Subset of ) ,(A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) \/ (Kurat14ClPart A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( non empty ) set ) \/ (Kurat14OpPart A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) set ) ;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Kurat14Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) -> finite ;
end;

theorem :: KURATO_1:6
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, Q being ( ( ) ( ) Subset of ) st Q : ( ( ) ( ) Subset of ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) holds
( Q : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) & Q : ( ( ) ( ) Subset of ) - : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat14Set A : ( ( ) ( ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) ) ;

theorem :: KURATO_1:7
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds card (Kurat14Set A : ( ( ) ( ) Subset of ) ) : ( ( ) ( finite ) Subset-Family of ) : ( ( ) ( ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) set ) ) <= 14 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
func Kurat7Set A -> ( ( ) ( ) Subset-Family of ) equals :: KURATO_1:def 5
{A : ( ( non empty ) ( non empty ) set ) ,(Int A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int (Cl A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl (Int A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) ;
end;

theorem :: KURATO_1:8
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Kurat7Set A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) = ({A : ( ( ) ( ) Subset of ) } : ( ( ) ( non empty finite ) set ) \/ {(Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty finite ) set ) \/ {(Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) : ( ( ) ( non empty finite ) set ) ;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Kurat7Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) -> finite ;
end;

theorem :: KURATO_1:9
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, Q being ( ( ) ( ) Subset of ) st Q : ( ( ) ( ) Subset of ) in Kurat7Set A : ( ( ) ( ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) holds
( Int Q : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat7Set A : ( ( ) ( ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) & Cl Q : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in Kurat7Set A : ( ( ) ( ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) ) ;

begin

definition
func KurExSet -> ( ( ) ( V136() V137() V138() ) Subset of ) equals :: KURATO_1:def 6
(({1 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ (RAT (2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: KURATO_1:10
Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = {1 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ [.2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:11
(Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,1 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].1 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:12
Cl ((Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:13
(Cl ((Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:14
Cl ((Cl ((Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = [.2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:15
(Cl ((Cl ((Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:16
KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ` : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = (((].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,1 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].1 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ {4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ {5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:17
Cl (KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ {5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:18
(Cl (KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:19
Cl ((Cl (KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = [.4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:20
(Cl ((Cl (KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:21
Cl ((Cl ((Cl (KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty ext-real non positive negative ) set ) ,4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:22
(Cl ((Cl ((Cl (KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: KURATO_1:23
Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].5 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:24
Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = [.4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:25
Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].4 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:26
Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = ].2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:27
Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) = [.2 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V136() V137() V138() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: KURATO_1:28
Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:29
Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:30
Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:31
Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:32
Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:33
Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:34
Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:35
Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:36
Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:37
Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:38
Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:39
Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:40
Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ;

theorem :: KURATO_1:41
KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) <> Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:42
Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:43
Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:44
Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: KURATO_1:45
Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) <> Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:46
Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) are_mutually_different ;

theorem :: KURATO_1:47
Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) are_mutually_different ;

theorem :: KURATO_1:48
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in {(Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) holds
X : ( ( ) ( ) set ) is ( ( non empty open ) ( non empty open V136() V137() V138() ) Subset of ) ;

theorem :: KURATO_1:49
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in {(Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) holds
X : ( ( ) ( ) set ) <> REAL : ( ( ) ( V136() V137() V138() V142() ) set ) ;

theorem :: KURATO_1:50
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in {(Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) holds
X : ( ( ) ( ) set ) <> REAL : ( ( ) ( V136() V137() V138() V142() ) set ) ;

theorem :: KURATO_1:51
{(Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) misses {(Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) ;

theorem :: KURATO_1:52
Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Int (Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl (Int KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl (Int (Cl KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) are_mutually_different ;

registration
cluster KurExSet : ( ( ) ( V136() V137() V138() ) Subset of ) -> non open non closed ;
end;

theorem :: KURATO_1:53
{(Int KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Int (Cl (Int KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ,(Cl (Int (Cl KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) misses {KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) } : ( ( ) ( non empty finite ) set ) ;

theorem :: KURATO_1:54
KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) , Int KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Int (Cl KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Int (Cl (Int KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl (Int KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) , Cl (Int (Cl KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) are_mutually_different ;

theorem :: KURATO_1:55
card (Kurat7Set KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( finite ) Subset-Family of ) : ( ( ) ( ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) set ) ) = 7 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

begin

registration
cluster Kurat14ClPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( ) Subset-Family of ) -> with_proper_subsets ;
cluster Kurat14OpPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( ) Subset-Family of ) -> with_proper_subsets ;
end;

registration
cluster Kurat14Set KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( finite ) Subset-Family of ) -> with_proper_subsets ;
end;

registration
cluster Kurat14Set KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_proper_subsets finite ) Subset-Family of ) -> with_non-empty_elements ;
end;

theorem :: KURATO_1:56
for A being ( ( with_non-empty_elements ) ( with_non-empty_elements ) set )
for B being ( ( ) ( ) set ) st B : ( ( ) ( ) set ) c= A : ( ( with_non-empty_elements ) ( with_non-empty_elements ) set ) holds
B : ( ( ) ( ) set ) is with_non-empty_elements ;

registration
cluster Kurat14ClPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_proper_subsets ) Subset-Family of ) -> with_non-empty_elements ;
cluster Kurat14OpPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_proper_subsets ) Subset-Family of ) -> with_non-empty_elements ;
end;

registration
cluster with_non-empty_elements with_proper_subsets for ( ( ) ( ) Element of bool (bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: KURATO_1:57
for F, G being ( ( with_non-empty_elements with_proper_subsets ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) st F : ( ( with_non-empty_elements with_proper_subsets ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) is open & G : ( ( with_non-empty_elements with_proper_subsets ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) is closed holds
F : ( ( with_non-empty_elements with_proper_subsets ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) misses G : ( ( with_non-empty_elements with_proper_subsets ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) ;

registration
cluster Kurat14ClPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) -> closed ;
cluster Kurat14OpPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_non-empty_elements with_proper_subsets ) Subset-Family of ) -> open ;
end;

theorem :: KURATO_1:58
Kurat14ClPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_non-empty_elements with_proper_subsets closed ) Subset-Family of ) misses Kurat14OpPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_non-empty_elements with_proper_subsets open ) Subset-Family of ) ;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Kurat14ClPart A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) -> finite ;
cluster Kurat14OpPart A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) -> finite ;
end;

theorem :: KURATO_1:59
card (Kurat14ClPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( with_non-empty_elements with_proper_subsets finite closed ) Subset-Family of ) : ( ( ) ( ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) set ) ) = 6 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: KURATO_1:60
card (Kurat14OpPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( with_non-empty_elements with_proper_subsets finite open ) Subset-Family of ) : ( ( ) ( ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) set ) ) = 6 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: KURATO_1:61
{KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) ,(KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) misses Kurat14ClPart KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_non-empty_elements with_proper_subsets finite closed ) Subset-Family of ) ;

registration
cluster KurExSet : ( ( ) ( non open non closed V136() V137() V138() ) Subset of ) -> non empty ;
end;

theorem :: KURATO_1:62
KurExSet : ( ( ) ( non empty non open non closed V136() V137() V138() ) Subset of ) <> KurExSet : ( ( ) ( non empty non open non closed V136() V137() V138() ) Subset of ) ` : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_1:63
{KurExSet : ( ( ) ( non empty non open non closed V136() V137() V138() ) Subset of ) ,(KurExSet : ( ( ) ( non empty non open non closed V136() V137() V138() ) Subset of ) `) : ( ( ) ( V136() V137() V138() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V122() ) TopStruct ) : ( ( ) ( non empty V136() V137() V138() ) set ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) misses Kurat14OpPart KurExSet : ( ( ) ( non empty non open non closed V136() V137() V138() ) Subset of ) : ( ( ) ( with_non-empty_elements with_proper_subsets finite open ) Subset-Family of ) ;

theorem :: KURATO_1:64
card (Kurat14Set KurExSet : ( ( ) ( non empty non open non closed V136() V137() V138() ) Subset of ) ) : ( ( ) ( with_non-empty_elements with_proper_subsets finite ) Subset-Family of ) : ( ( ) ( ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) set ) ) = 14 : ( ( ) ( non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() ) Element of NAT : ( ( ) ( V136() V137() V138() V139() V140() V141() V142() ) Element of bool REAL : ( ( ) ( V136() V137() V138() V142() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let T be ( ( ) ( ) TopStruct ) ;
let A be ( ( ) ( ) Subset-Family of ) ;
attr A is Cl-closed means :: KURATO_1:def 7
 for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) in A : ( ( non empty ) ( non empty ) set ) holds
Cl P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) set ) ;
attr A is Int-closed means :: KURATO_1:def 8
 for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) in A : ( ( non empty ) ( non empty ) set ) holds
Int P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of T : ( ( cardinal ) ( cardinal ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) set ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Kurat14Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Subset-Family of ) -> non empty ;
cluster Kurat14Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Subset-Family of ) -> Cl-closed ;
cluster Kurat14Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Subset-Family of ) -> compl-closed ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Kurat7Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Subset-Family of ) -> non empty ;
cluster Kurat7Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Subset-Family of ) -> Int-closed ;
cluster Kurat7Set A : ( ( ) ( ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Subset-Family of ) -> Cl-closed ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster non empty Cl-closed Int-closed for ( ( ) ( ) Element of bool (bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
cluster non empty compl-closed Cl-closed for ( ( ) ( ) Element of bool (bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;