:: TOPS_2 semantic presentation

begin

theorem :: TOPS_2:1
for T being ( ( ) ( ) 1-sorted )
for F being ( ( ) ( ) Subset-Family of ) holds F : ( ( ) ( ) Subset-Family of ) c= bool ([#] T : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool ([#] b1 : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:2
for T being ( ( ) ( ) 1-sorted )
for F being ( ( ) ( ) Subset-Family of )
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= F : ( ( ) ( ) Subset-Family of ) holds
X : ( ( ) ( ) set ) is ( ( ) ( ) Subset-Family of ) ;

theorem :: TOPS_2:3
for T being ( ( non empty ) ( non empty ) 1-sorted )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty ) set ) ) holds
F : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) ;

theorem :: TOPS_2:4
for T being ( ( ) ( ) 1-sorted )
for F, G being ( ( ) ( ) Subset-Family of ) holds (union F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \ (union G : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= union (F : ( ( ) ( ) Subset-Family of ) \ G : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:5
for T being ( ( ) ( ) set )
for F being ( ( ) ( ) Subset-Family of ) holds
( F : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) iff COMPLEMENT F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) ) ;

theorem :: TOPS_2:6
for T being ( ( ) ( ) set )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) holds
meet (COMPLEMENT F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (union F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:7
for T being ( ( ) ( ) set )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) holds
union (COMPLEMENT F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (meet F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:8
for T being ( ( ) ( ) 1-sorted )
for F being ( ( ) ( ) Subset-Family of ) holds
( COMPLEMENT F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is finite iff F : ( ( ) ( ) Subset-Family of ) is finite ) ;

definition
let T be ( ( ) ( ) TopStruct ) ;
let F be ( ( ) ( ) Subset-Family of ) ;
attr F is open means :: TOPS_2:def 1
 for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
P : ( ( ) ( ) Subset of ) is open ;
attr F is closed means :: TOPS_2:def 2
 for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
P : ( ( ) ( ) Subset of ) is closed ;
end;

theorem :: TOPS_2:9
for T being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of ) holds
( F : ( ( ) ( ) Subset-Family of ) is closed iff COMPLEMENT F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ) ;

theorem :: TOPS_2:10
for T being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of ) holds
( F : ( ( ) ( ) Subset-Family of ) is open iff COMPLEMENT F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ) ;

theorem :: TOPS_2:11
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) c= G : ( ( ) ( ) Subset-Family of ) & G : ( ( ) ( ) Subset-Family of ) is open holds
F : ( ( ) ( ) Subset-Family of ) is open ;

theorem :: TOPS_2:12
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) c= G : ( ( ) ( ) Subset-Family of ) & G : ( ( ) ( ) Subset-Family of ) is closed holds
F : ( ( ) ( ) Subset-Family of ) is closed ;

theorem :: TOPS_2:13
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is open & G : ( ( ) ( ) Subset-Family of ) is open holds
F : ( ( ) ( ) Subset-Family of ) \/ G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ;

theorem :: TOPS_2:14
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is open holds
F : ( ( ) ( ) Subset-Family of ) /\ G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ;

theorem :: TOPS_2:15
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is open holds
F : ( ( ) ( ) Subset-Family of ) \ G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ;

theorem :: TOPS_2:16
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is closed & G : ( ( ) ( ) Subset-Family of ) is closed holds
F : ( ( ) ( ) Subset-Family of ) \/ G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

theorem :: TOPS_2:17
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is closed holds
F : ( ( ) ( ) Subset-Family of ) /\ G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

theorem :: TOPS_2:18
for T being ( ( ) ( ) TopStruct )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is closed holds
F : ( ( ) ( ) Subset-Family of ) \ G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

theorem :: TOPS_2:19
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for W being ( ( ) ( ) Subset-Family of ) st W : ( ( ) ( ) Subset-Family of ) is open holds
union W : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open ;

theorem :: TOPS_2:20
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for W being ( ( ) ( ) Subset-Family of ) st W : ( ( ) ( ) Subset-Family of ) is open & W : ( ( ) ( ) Subset-Family of ) is finite holds
meet W : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open ;

theorem :: TOPS_2:21
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for W being ( ( ) ( ) Subset-Family of ) st W : ( ( ) ( ) Subset-Family of ) is closed & W : ( ( ) ( ) Subset-Family of ) is finite holds
union W : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

theorem :: TOPS_2:22
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for W being ( ( ) ( ) Subset-Family of ) st W : ( ( ) ( ) Subset-Family of ) is closed holds
meet W : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed ;

theorem :: TOPS_2:23
for T being ( ( ) ( ) TopStruct )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) )
for F being ( ( ) ( ) Subset-Family of ) holds F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Subset-Family of ) ;

theorem :: TOPS_2:24
for T being ( ( ) ( ) TopStruct )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) )
for B being ( ( ) ( ) Subset of ) holds
( B : ( ( ) ( ) Subset of ) is open iff ex C being ( ( ) ( ) Subset of ) st
( C : ( ( ) ( ) Subset of ) is open & C : ( ( ) ( ) Subset of ) /\ ([#] A : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = B : ( ( ) ( ) Subset of ) ) ) ;

theorem :: TOPS_2:25
for T being ( ( ) ( ) TopStruct )
for Q being ( ( ) ( ) Subset of )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) ) st Q : ( ( ) ( ) Subset of ) is open holds
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = Q : ( ( ) ( ) Subset of ) holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: TOPS_2:26
for T being ( ( ) ( ) TopStruct )
for Q being ( ( ) ( ) Subset of )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) ) st Q : ( ( ) ( ) Subset of ) is closed holds
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = Q : ( ( ) ( ) Subset of ) holds
P : ( ( ) ( ) Subset of ) is closed ;

theorem :: TOPS_2:27
for T being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) ) st F : ( ( ) ( ) Subset-Family of ) is open holds
for G being ( ( ) ( ) Subset-Family of ) st G : ( ( ) ( ) Subset-Family of ) = F : ( ( ) ( ) Subset-Family of ) holds
G : ( ( ) ( ) Subset-Family of ) is open ;

theorem :: TOPS_2:28
for T being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) ) st F : ( ( ) ( ) Subset-Family of ) is closed holds
for G being ( ( ) ( ) Subset-Family of ) st G : ( ( ) ( ) Subset-Family of ) = F : ( ( ) ( ) Subset-Family of ) holds
G : ( ( ) ( ) Subset-Family of ) is closed ;

theorem :: TOPS_2:29
for T being ( ( ) ( ) TopStruct )
for M, N being ( ( ) ( ) Subset of ) holds M : ( ( ) ( ) Subset of ) /\ N : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Subset of ) ;

definition
let T be ( ( ) ( ) TopStruct ) ;
let P be ( ( ) ( ) Subset of ) ;
let F be ( ( ) ( ) Subset-Family of ) ;
func F | P -> ( ( ) ( ) Subset-Family of ) means :: TOPS_2:def 3
 for Q being ( ( ) ( ) Subset of ) holds
( Q : ( ( ) ( ) Subset of ) in it : ( ( ) ( ) set ) iff ex R being ( ( ) ( ) Subset of ) st
( R : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Element of T : ( ( ) ( ) TopStruct ) ) & R : ( ( ) ( ) Subset of ) /\ P : ( ( ) ( ) Element of bool (bool T : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Q : ( ( ) ( ) Subset of ) ) );
end;

theorem :: TOPS_2:30
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F, G being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) c= G : ( ( ) ( ) Subset-Family of ) holds
F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) c= G : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: TOPS_2:31
for T being ( ( ) ( ) TopStruct )
for Q, M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st Q : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Subset-Family of ) holds
Q : ( ( ) ( ) Subset of ) /\ M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) ;

theorem :: TOPS_2:32
for T being ( ( ) ( ) TopStruct )
for Q, M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st Q : ( ( ) ( ) Subset of ) c= union F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
Q : ( ( ) ( ) Subset of ) /\ M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= union (F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of (b1 : ( ( ) ( ) TopStruct ) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:33
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st M : ( ( ) ( ) Subset of ) c= union F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
M : ( ( ) ( ) Subset of ) = union (F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of (b1 : ( ( ) ( ) TopStruct ) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:34
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) holds union (F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of (b1 : ( ( ) ( ) TopStruct ) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= union F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:35
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st M : ( ( ) ( ) Subset of ) c= union (F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of (b1 : ( ( ) ( ) TopStruct ) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
M : ( ( ) ( ) Subset of ) c= union F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:36
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is finite holds
F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) is finite ;

theorem :: TOPS_2:37
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is open holds
F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) is open ;

theorem :: TOPS_2:38
for T being ( ( ) ( ) TopStruct )
for M being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is closed holds
F : ( ( ) ( ) Subset-Family of ) | M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) is closed ;

theorem :: TOPS_2:39
for T being ( ( ) ( ) TopStruct )
for A being ( ( ) ( ) SubSpace of T : ( ( ) ( ) TopStruct ) )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is open holds
ex G being ( ( ) ( ) Subset-Family of ) st
( G : ( ( ) ( ) Subset-Family of ) is open & ( for AA being ( ( ) ( ) Subset of ) st AA : ( ( ) ( ) Subset of ) = [#] A : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) SubSpace of b1 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
F : ( ( ) ( ) Subset-Family of ) = G : ( ( ) ( ) Subset-Family of ) | AA : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) ) ) ;

theorem :: TOPS_2:40
for T being ( ( ) ( ) TopStruct )
for P being ( ( ) ( ) Subset of )
for F being ( ( ) ( ) Subset-Family of ) ex f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = F : ( ( ) ( ) Subset-Family of ) & rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = F : ( ( ) ( ) Subset-Family of ) | P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset-Family of ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in F : ( ( ) ( ) Subset-Family of ) holds
for Q being ( ( ) ( ) Subset of ) st Q : ( ( ) ( ) Subset of ) = x : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Q : ( ( ) ( ) Subset of ) /\ P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: TOPS_2:41
for X, Y being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st ( [#] Y : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) implies [#] X : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) " ([#] Y : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] X : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:42
for T being ( ( ) ( ) 1-sorted )
for S being ( ( non empty ) ( non empty ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for H being ( ( ) ( ) Subset-Family of ) holds (" f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: H : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) set ) is ( ( ) ( ) Subset-Family of ) ;

theorem :: TOPS_2:43
for X, Y being ( ( ) ( ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st ( [#] Y : ( ( ) ( ) TopStruct ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) implies [#] X : ( ( ) ( ) TopStruct ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding K123() : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool K119() : ( ( ) ( V36() V37() V38() V42() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like one-to-one constant functional V36() V37() V38() V39() V40() V41() V42() finite FinSequence-like FinSubsequence-like FinSequence-membered ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous iff for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) is open holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) " P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open ) ;

theorem :: TOPS_2:44
for T, S being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous iff for P1 being ( ( ) ( ) Subset of ) holds Cl (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) " P1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) " (Cl P1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPS_2:45
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous iff for P being ( ( ) ( ) Subset of ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: (Cl P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= Cl (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPS_2:46
errorfrm ;

theorem :: TOPS_2:47
for T being ( ( ) ( ) TopStruct )
for S being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for H being ( ( ) ( ) Subset-Family of ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is continuous & H : ( ( ) ( ) Subset-Family of ) is open holds
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) = (" f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: H : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) set ) holds
F : ( ( ) ( ) Subset-Family of ) is open ;

theorem :: TOPS_2:48
for T, S being ( ( ) ( ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for H being ( ( ) ( ) Subset-Family of ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous & H : ( ( ) ( ) Subset-Family of ) is closed holds
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) = (" f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: H : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) set ) holds
F : ( ( ) ( ) Subset-Family of ) is closed ;

definition
let S, T be ( ( ) ( ) set ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like S : ( ( ) ( ) set ) -defined T : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of S : ( ( ) ( ) set ) ,T : ( ( ) ( ) set ) ) ;
assume f : ( ( Function-like quasi_total ) ( Relation-like S : ( ( ) ( ) set ) -defined T : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of S : ( ( ) ( ) set ) ,T : ( ( ) ( ) set ) ) is bijective ;
func f /" -> ( ( Function-like quasi_total ) ( Relation-like T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined S : ( ( ) ( ) TopStruct ) -valued Function-like quasi_total ) Function of T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,S : ( ( ) ( ) TopStruct ) ) equals :: TOPS_2:def 4
f : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;
end;

notation
let S, T be ( ( ) ( ) set ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like S : ( ( ) ( ) set ) -defined T : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of S : ( ( ) ( ) set ) ,T : ( ( ) ( ) set ) ) ;
synonym f " for f /" ;
end;

theorem :: TOPS_2:49
for T being ( ( ) ( ) 1-sorted )
for S being ( ( non empty ) ( non empty ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one holds
( dom (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & rng (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPS_2:50
for T, S being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is one-to-one holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is one-to-one ;

theorem :: TOPS_2:51
for T being ( ( ) ( ) 1-sorted )
for S being ( ( non empty ) ( non empty ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one holds
(f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:52
for T, S being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is one-to-one holds
( (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = id (dom f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( V17( dom b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like dom b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined dom b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one V17( dom b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(dom b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(dom b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) * (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = id (rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( V17( rng b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like rng b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined rng b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one V17( rng b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(rng b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(rng b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPS_2:53
for T being ( ( ) ( ) 1-sorted )
for S, V being ( ( non empty ) ( non empty ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & dom g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & rng g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] V : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one holds
(g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) * (g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier of b3 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:54
for T, S being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for P being ( ( ) ( ) Subset of ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is one-to-one holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) .: P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) " P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPS_2:55
for T, S being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for P1 being ( ( ) ( ) Subset of ) st rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of bool the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is one-to-one holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) " P1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) .: P1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let S, T be ( ( ) ( ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr f is being_homeomorphism means :: TOPS_2:def 5
( dom f : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) Element of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( ) ( ) TopStruct ) : ( ( ) ( non proper ) Element of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & rng f : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) is one-to-one & f : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) is continuous & f : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) is continuous );
end;

theorem :: TOPS_2:56
for T being ( ( ) ( ) TopStruct )
for S being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) is being_homeomorphism ;

theorem :: TOPS_2:57
errorfrm ;

theorem :: TOPS_2:58
for T being ( ( ) ( ) TopStruct )
for S being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism iff ( dom f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( ) ( ) TopStruct ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty non proper ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & ( for P being ( ( ) ( ) Subset of ) holds
( P : ( ( ) ( ) Subset of ) is closed iff f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ) ) ) ) ;

theorem :: TOPS_2:59
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism iff ( dom f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper closed ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non proper closed ) Element of bool the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is one-to-one & ( for P1 being ( ( ) ( ) Subset of ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) " (Cl P1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Cl (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) " P1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: TOPS_2:60
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism iff ( dom f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non proper closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper closed ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & ( for P being ( ( ) ( ) Subset of ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: (Cl P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Cl (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) .: P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: TOPS_2:61
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & A : ( ( ) ( ) Subset of ) is connected holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is connected ;

theorem :: TOPS_2:62
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & A : ( ( ) ( ) Subset of ) is connected holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " 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 ) ) is connected ;

begin

theorem :: TOPS_2:63
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st ( for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ex GY being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st
( GY : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is connected & ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) holds
GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is connected ;

theorem :: TOPS_2:64
for X being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of ) holds
( F : ( ( ) ( ) Subset-Family of ) is open iff F : ( ( ) ( ) Subset-Family of ) c= the topology of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPS_2:65
for X being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of ) holds
( F : ( ( ) ( ) Subset-Family of ) is closed iff F : ( ( ) ( ) Subset-Family of ) c= COMPLEMENT the topology of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

registration
let X be ( ( ) ( ) TopStruct ) ;
cluster the topology of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> open ;
cluster open for ( ( ) ( ) Element of bool (bool the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;