CANTOR_1

:: CANTOR_1 semantic presentation

begin

definition

let X be ( ( ) ( ) set ) ;
let A be ( ( ) ( ) Subset-Family of ) ;

func UniCl A -> ( ( ) ( ) Subset-Family of ) means :: CANTOR_1:def 1
for x being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) Element of X : ( ( ) ( ) TopStruct ) ) iff ex Y being ( ( ) ( ) Subset-Family of ) st
( Y : ( ( ) ( ) Subset-Family of ) c= A : ( ( ) ( ) Element of bool (bool X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = union Y : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool X : ( ( ) ( ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) );

end;

definition

let X be ( ( ) ( ) TopStruct ) ;
let F be ( ( ) ( ) Subset-Family of ) ;

attr F is quasi_basis means :: CANTOR_1:def 2
the topology of X : ( ( ) ( ) TopStruct ) : ( ( ) ( open ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= UniCl F : ( ( ) ( ) Element of bool (bool X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) ;

end;

registration

let X be ( ( ) ( ) TopStruct ) ;

cluster the topology of X : ( ( ) ( ) TopStruct ) : ( ( ) ( open ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> quasi_basis ;

end;

registration

let X be ( ( ) ( ) TopStruct ) ;

cluster open quasi_basis for ( ( ) ( ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

let X be ( ( ) ( ) TopStruct ) ;
mode Basis of X is ( ( open quasi_basis ) ( open quasi_basis ) Subset-Family of ) ;

end;

theorem :: CANTOR_1:1

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of ) holds A : ( ( ) ( ) Subset-Family of ) c= UniCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:2

for S being ( ( ) ( ) TopStruct ) holds the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( open quasi_basis ) ( open quasi_basis ) Basis of S : ( ( ) ( ) TopStruct ) ) ;

theorem :: CANTOR_1:3

for S being ( ( ) ( ) TopStruct ) holds the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ;

definition

let X be ( ( ) ( ) set ) ;
let A be ( ( ) ( ) Subset-Family of ) ;

func FinMeetCl A -> ( ( ) ( ) Subset-Family of ) means :: CANTOR_1:def 3
for x being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) Element of X : ( ( ) ( ) TopStruct ) ) iff ex Y being ( ( ) ( ) Subset-Family of ) st
( Y : ( ( ) ( ) Subset-Family of ) c= A : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) & Y : ( ( ) ( ) Subset-Family of ) is finite & x : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = Intersect Y : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool X : ( ( ) ( ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) );

end;

theorem :: CANTOR_1:4

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of ) holds A : ( ( ) ( ) Subset-Family of ) c= FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:5

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = FinMeetCl the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:6

for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = UniCl the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:7

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = UniCl (FinMeetCl the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open quasi_basis ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:8

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of ) holds X : ( ( ) ( ) set ) in FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:9

for X being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset-Family of ) st A : ( ( ) ( ) Subset-Family of ) c= B : ( ( ) ( ) Subset-Family of ) holds
UniCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) c= UniCl B : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:10

for X being ( ( ) ( ) set )
for R being ( ( non empty ) ( non empty ) Subset-Family of )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) = { (Intersect x : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of R : ( ( non empty ) ( non empty ) Subset-Family of ) ) : verum } holds
Intersect F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Intersect (union R : ( ( non empty ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: CANTOR_1:11

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of ) holds FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) = FinMeetCl (FinMeetCl A : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:12

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of )
for a, b being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) & b : ( ( ) ( ) set ) in FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) holds
a : ( ( ) ( ) set ) /\ b : ( ( ) ( ) set ) : ( ( ) ( ) set ) in FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:13

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of )
for a, b being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) c= FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) & b : ( ( ) ( ) set ) c= FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) holds
INTERSECTION (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: CANTOR_1:14

for X being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset-Family of ) st A : ( ( ) ( ) Subset-Family of ) c= B : ( ( ) ( ) Subset-Family of ) holds
FinMeetCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) c= FinMeetCl B : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Subset-Family of ) ;

registration

let X be ( ( ) ( ) set ) ;
let A be ( ( ) ( ) Subset-Family of ) ;

cluster FinMeetCl A : ( ( ) ( ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset-Family of ) -> non empty ;

end;

theorem :: CANTOR_1:15

for X being ( ( non empty ) ( non empty ) set )
for A being ( ( ) ( ) Subset-Family of ) holds TopStruct(# X : ( ( non empty ) ( non empty ) set ) ,(UniCl (FinMeetCl A : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( non empty strict ) TopStruct ) is TopSpace-like ;

definition

let X be ( ( ) ( ) TopStruct ) ;
let F be ( ( ) ( ) Subset-Family of ) ;

attr F is quasi_prebasis means :: CANTOR_1:def 4
ex G being ( ( open quasi_basis ) ( open quasi_basis ) Basis of X : ( ( ) ( ) TopStruct ) ) st G : ( ( open quasi_basis ) ( open quasi_basis ) Basis of X : ( ( ) ( ) TopStruct ) ) c= FinMeetCl F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) Subset-Family of ) ;

end;

registration

let X be ( ( ) ( ) TopStruct ) ;

cluster the topology of X : ( ( ) ( ) TopStruct ) : ( ( ) ( open quasi_basis ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> quasi_prebasis ;

cluster open quasi_basis -> open quasi_basis quasi_prebasis for ( ( ) ( ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

cluster open quasi_prebasis for ( ( ) ( ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

let X be ( ( ) ( ) TopStruct ) ;
mode prebasis of X is ( ( open quasi_prebasis ) ( open quasi_prebasis ) Subset-Family of ) ;

end;

theorem :: CANTOR_1:16

for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( ) ( ) Subset-Family of ) holds Y : ( ( ) ( ) Subset-Family of ) is ( ( open quasi_basis ) ( open quasi_basis quasi_prebasis ) Basis of TopStruct(# X : ( ( non empty ) ( non empty ) set ) ,(UniCl Y : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( non empty strict ) TopStruct ) ) ;

theorem :: CANTOR_1:17

for T1, T2 being ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace)
for P being ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of T1 : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) ) st the carrier of T1 : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) : ( ( ) ( ) set ) = the carrier of T2 : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) : ( ( ) ( ) set ) & P : ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of b₁ : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) ) is ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of T2 : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) ) holds
T1 : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) = T2 : ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) ;

theorem :: CANTOR_1:18

for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( ) ( ) Subset-Family of ) holds Y : ( ( ) ( ) Subset-Family of ) is ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of TopStruct(# X : ( ( non empty ) ( non empty ) set ) ,(UniCl (FinMeetCl Y : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( non empty strict ) TopStruct ) ) ;

definition

func the_Cantor_set -> ( ( non empty strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) means :: CANTOR_1:def 5
( the carrier of it : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) = product (NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional with_common_domain product-like ) set ) & ex P being ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of it : ( ( ) ( ) TopStruct ) ) st
for X being ( ( ) ( functional with_common_domain ) Subset of ( ( ) ( non empty ) set ) ) holds
( X : ( ( ) ( functional with_common_domain ) Subset of ( ( ) ( non empty ) set ) ) in P : ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of ) iff ex N, n being ( ( V37() ) ( V37() ) Nat) st
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -compatible V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of product (NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional with_common_domain product-like ) set ) ) holds
( F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -compatible V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of product (NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional with_common_domain product-like ) set ) ) in X : ( ( ) ( functional with_common_domain ) Subset of ( ( ) ( non empty ) set ) ) iff F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -compatible V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of product (NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) --> {0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) ) : ( ( Function-like V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) ) ( non trivial Relation-like non-empty NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) -valued Function-like constant V17( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V21( NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) ) non finite ) Element of bool [:NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,{{0 : ( ( ) ( empty Function-like functional finite V42() countable ) Element of NAT : ( ( ) ( non trivial non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite countable ) set ) } : ( ( ) ( non empty finite V42() countable ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional with_common_domain product-like ) set ) ) . N : ( ( V37() ) ( V37() ) Nat) : ( ( ) ( ) set ) = n : ( ( V37() ) ( V37() ) Nat) ) ) );

end;