:: PENCIL_1 semantic presentation

begin

theorem :: PENCIL_1:1
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st product f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( functional with_common_domain product-like ) set ) = product g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( functional with_common_domain product-like ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is non-empty holds
g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is non-empty ;

theorem :: PENCIL_1:2
for X being ( ( ) ( ) set ) holds
( 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) iff ex x, y being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) ) ) ;

theorem :: PENCIL_1:3
for X being ( ( ) ( ) set ) st 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) holds
for x being ( ( ) ( ) set ) ex y being ( ( ) ( ) set ) st
( y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) ) ;

theorem :: PENCIL_1:4
for X being ( ( ) ( ) set ) holds
( 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) iff not X : ( ( ) ( ) set ) is trivial ) ;

theorem :: PENCIL_1:5
for X being ( ( ) ( ) set ) holds
( 3 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) iff ex x, y, z being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) <> z : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) <> z : ( ( ) ( ) set ) ) ) ;

theorem :: PENCIL_1:6
for X being ( ( ) ( ) set ) st 3 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) holds
for x, y being ( ( ) ( ) set ) ex z being ( ( ) ( ) set ) st
( z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) <> z : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) <> z : ( ( ) ( ) set ) ) ;

begin

definition
let S be ( ( ) ( ) TopStruct ) ;
mode Block of S is ( ( ) ( ) Element of the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let S be ( ( ) ( ) TopStruct ) ;
let x, y be ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;
pred x,y are_collinear means :: PENCIL_1:def 1
( x : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) or ex l being ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) st {x : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of S : ( ( ) ( ) TopStruct ) ) } : ( ( ) ( non empty finite countable ) set ) c= l : ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) );
end;

definition
let S be ( ( ) ( ) TopStruct ) ;
let T be ( ( ) ( ) Subset of ) ;
attr T is closed_under_lines means :: PENCIL_1:def 2
 for l being ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) st 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card (l : ( ( ) ( ) Point of ( ( ) ( ) set ) ) /\ T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) holds
l : ( ( ) ( ) Point of ( ( ) ( ) set ) ) c= T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
attr T is strong means :: PENCIL_1:def 3
 for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) are_collinear ;
end;

definition
let S be ( ( ) ( ) TopStruct ) ;
attr S is void means :: PENCIL_1:def 4
 the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is empty ;
attr S is degenerated means :: PENCIL_1:def 5
 the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) is ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) ;
attr S is with_non_trivial_blocks means :: PENCIL_1:def 6
 for k being ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) holds 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card k : ( ( ) ( ) Point of ( ( ) ( ) set ) ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) ;
attr S is identifying_close_blocks means :: PENCIL_1:def 7
 for k, l being ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) st 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card (k : ( ( ) ( ) Point of ( ( ) ( ) set ) ) /\ l : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) holds
k : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = l : ( ( ) ( ) Subset of ) ;
attr S is truly-partial means :: PENCIL_1:def 8
 not for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Subset of ) are_collinear ;
attr S is without_isolated_points means :: PENCIL_1:def 9
 for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) ex l being ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) ) st x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in l : ( ( ) ( ) Subset of ) ;
attr S is connected means :: PENCIL_1:def 10
 for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) ex f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) st
( x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & y : ( ( ) ( ) Subset of ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . (len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & ( for i being ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) st 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) & i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) < len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for a, b being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) : ( ( ) ( ) set ) & b : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . (i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) + 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) holds
a : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( ) set ) ) are_collinear ) );
attr S is strongly_connected means :: PENCIL_1:def 11
 for x being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is closed_under_lines & X : ( ( ) ( ) Subset of ) is strong holds
ex f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st
( X : ( ( ) ( ) Subset of ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . (len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & ( for W being ( ( ) ( ) Subset of ) st W : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) in rng f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
( W : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) is closed_under_lines & W : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) is strong ) ) & ( for i being ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) st 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) & i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) < len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card ((f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) ) : ( ( ) ( ) set ) /\ (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of bool the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . (i : ( ( V27() ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Nat) + 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) ) );
end;

theorem :: PENCIL_1:7
for X being ( ( non empty ) ( non empty ) set ) st 3 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( non empty ) ( non empty ) set ) : ( ( cardinal ) ( non empty V21() V22() V23() cardinal ) set ) holds
for S being ( ( ) ( ) TopStruct ) st the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) = X : ( ( non empty ) ( non empty ) set ) & the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = { L : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where L is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = card L : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) } holds
( not S : ( ( ) ( ) TopStruct ) is empty & not S : ( ( ) ( ) TopStruct ) is void & not S : ( ( ) ( ) TopStruct ) is degenerated & not S : ( ( ) ( ) TopStruct ) is truly-partial & S : ( ( ) ( ) TopStruct ) is with_non_trivial_blocks & S : ( ( ) ( ) TopStruct ) is identifying_close_blocks & S : ( ( ) ( ) TopStruct ) is without_isolated_points ) ;

theorem :: PENCIL_1:8
for X being ( ( non empty ) ( non empty ) set ) st 3 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card X : ( ( non empty ) ( non empty ) set ) : ( ( cardinal ) ( non empty V21() V22() V23() cardinal ) set ) holds
for K being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st card K : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) = 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for S being ( ( ) ( ) TopStruct ) st the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) = X : ( ( non empty ) ( non empty ) set ) & the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b3 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = { L : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where L is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = card L : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) } \ {K : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element countable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool { b4 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where L is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = card b4 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) } : ( ( ) ( non empty ) set ) ) holds
( not S : ( ( ) ( ) TopStruct ) is empty & not S : ( ( ) ( ) TopStruct ) is void & not S : ( ( ) ( ) TopStruct ) is degenerated & S : ( ( ) ( ) TopStruct ) is truly-partial & S : ( ( ) ( ) TopStruct ) is with_non_trivial_blocks & S : ( ( ) ( ) TopStruct ) is identifying_close_blocks & S : ( ( ) ( ) TopStruct ) is without_isolated_points ) ;

registration
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points for ( ( ) ( ) TopStruct ) ;
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points for ( ( ) ( ) TopStruct ) ;
end;

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

definition
let S be ( ( without_isolated_points ) ( without_isolated_points ) TopStruct ) ;
let x, y be ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;
redefine pred x,y are_collinear means :: PENCIL_1:def 12
 ex l being ( ( ) ( ) Block of S : ( ( ) ( ) set ) ) st {x : ( ( non empty ) ( non empty ) set ) ,y : ( ( ) ( ) Element of S : ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite countable ) set ) c= l : ( ( ) ( ) Block of S : ( ( without_isolated_points ) ( without_isolated_points ) TopStruct ) ) ;
end;

definition
mode PLS is ( ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) TopStruct ) ;
end;

definition
let F be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr F is TopStruct-yielding means :: PENCIL_1:def 13
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) TopStruct ) ;
end;

registration
cluster Relation-like Function-like TopStruct-yielding -> Relation-like Function-like 1-sorted-yielding for ( ( ) ( ) set ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) TopStruct-yielding for ( ( ) ( ) set ) ;
end;

registration
cluster Relation-like Function-like TopStruct-yielding for ( ( ) ( ) set ) ;
end;

definition
let F be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr F is non-void-yielding means :: PENCIL_1:def 14
 for S being ( ( ) ( ) TopStruct ) st S : ( ( ) ( ) TopStruct ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
not S : ( ( ) ( ) TopStruct ) is void ;
end;

definition
let F be ( ( Relation-like Function-like TopStruct-yielding ) ( Relation-like Function-like 1-sorted-yielding TopStruct-yielding ) Function) ;
redefine attr F is non-void-yielding means :: PENCIL_1:def 15
 for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
i : ( ( ) ( ) set ) is ( ( non void ) ( non void ) TopStruct ) ;
end;

definition
let F be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr F is trivial-yielding means :: PENCIL_1:def 16
 for S being ( ( ) ( ) set ) st S : ( ( ) ( ) set ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
S : ( ( ) ( ) set ) is trivial ;
end;

definition
let F be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr F is non-Trivial-yielding means :: PENCIL_1:def 17
 for S being ( ( ) ( ) 1-sorted ) st S : ( ( ) ( ) 1-sorted ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
not S : ( ( ) ( ) 1-sorted ) is trivial ;
end;

registration
cluster Relation-like non-Trivial-yielding -> Relation-like non-Empty for ( ( ) ( ) set ) ;
end;

definition
let F be ( ( Relation-like Function-like 1-sorted-yielding ) ( Relation-like Function-like 1-sorted-yielding ) Function) ;
redefine attr F is non-Trivial-yielding means :: PENCIL_1:def 18
 for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
i : ( ( ) ( ) set ) is ( ( non trivial ) ( non empty non trivial ) 1-sorted ) ;
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
let j be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func A . j -> ( ( ) ( ) TopStruct ) ;
end;

definition
let F be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr F is PLS-yielding means :: PENCIL_1:def 19
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in rng F : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) is ( ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) PLS) ;
end;

registration
cluster Relation-like Function-like PLS-yielding -> Relation-like Function-like non-Empty TopStruct-yielding for ( ( ) ( ) set ) ;
cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> Relation-like Function-like TopStruct-yielding non-void-yielding for ( ( ) ( ) set ) ;
cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> Relation-like Function-like TopStruct-yielding non-Trivial-yielding for ( ( ) ( ) set ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) PLS-yielding for ( ( ) ( ) set ) ;
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
let j be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func A . j -> ( ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) PLS) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let A be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
attr A is Segre-like means :: PENCIL_1:def 20
 ex i being ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) st
for j being ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) st i : ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) <> j : ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) holds
A : ( ( non empty ) ( non empty ) set ) . j : ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ;
end;

registration
let I be ( ( ) ( ) set ) ;
let A be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster {A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) } : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) finite-yielding ) set ) -> Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) trivial-yielding ;
end;

theorem :: PENCIL_1:9
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) )
for S being ( ( non trivial ) ( non empty non trivial ) set ) holds not A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) +* (i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,S : ( ( non trivial ) ( non empty non trivial ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) is trivial-yielding ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster {A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) } : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) finite-yielding trivial-yielding ) set ) -> Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) Segre-like ;
end;

theorem :: PENCIL_1:10
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for i, S being ( ( ) ( ) set ) holds {A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) finite-yielding trivial-yielding Segre-like ) set ) +* (i : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) is Segre-like ;

theorem :: PENCIL_1:11
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for B being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) Element of Carrier A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) holds {B : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) Element of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) } : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) finite-yielding trivial-yielding Segre-like ) set ) is ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSubset of Carrier A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster Relation-like V2() I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) trivial-yielding Segre-like for ( ( ) ( ) ManySortedSubset of Carrier A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty ) set ) : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) ) ;
end;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster Relation-like V2() I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like for ( ( ) ( ) ManySortedSubset of Carrier A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) set ) : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) ) ;
end;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
cluster Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like for ( ( ) ( ) set ) ;
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let B be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
func indx B -> ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) means :: PENCIL_1:def 21
 not B : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) set ) . it : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) is trivial ;
end;

theorem :: PENCIL_1:12
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) st i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) <> indx A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) holds
A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) is 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
cluster Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like -> Relation-like V2() I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) for ( ( ) ( ) set ) ;
end;

theorem :: PENCIL_1:13
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) holds
( 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card (product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( functional with_common_domain product-like ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) iff ( A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) is V2() & not A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) is trivial-yielding ) ) ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let B be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster product B : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) -> non trivial ;
end;

begin

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
func Segre_Blocks A -> ( ( ) ( ) Subset-Family of ) means :: PENCIL_1:def 22
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) iff ex B being ( ( Segre-like ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) Segre-like ) ManySortedSubset of Carrier A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) set ) : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) ) st
( x : ( ( ) ( ) set ) = product B : ( ( Segre-like ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) Segre-like ) ManySortedSubset of Carrier A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( functional with_common_domain product-like ) set ) & ex i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) st B : ( ( Segre-like ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) Segre-like ) ManySortedSubset of Carrier A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) ) . i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) is ( ( ) ( ) Block of (A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) set ) . i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) TopStruct ) ) ) );
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
func Segre_Product A -> ( ( non empty ) ( non empty ) TopStruct ) equals :: PENCIL_1:def 23
 TopStruct(# (product (Carrier A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) set ) ) : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ,(Segre_Blocks A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Trivial-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty non-Trivial-yielding ) set ) ) : ( ( ) ( ) Subset-Family of ) #) : ( ( strict ) ( strict ) TopStruct ) ;
end;

theorem :: PENCIL_1:14
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: PENCIL_1:15
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st not for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is void holds
not Segre_Product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) TopStruct ) is void ;

theorem :: PENCIL_1:16
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds
( not A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is degenerated & not for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is void ) ) holds
not Segre_Product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) TopStruct ) is degenerated ;

theorem :: PENCIL_1:17
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds
( A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is with_non_trivial_blocks & not for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is void ) ) holds
Segre_Product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) TopStruct ) is with_non_trivial_blocks ;

theorem :: PENCIL_1:18
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds
( A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is identifying_close_blocks & A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is with_non_trivial_blocks & not for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) TopStruct ) is void ) ) holds
Segre_Product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) TopStruct ) is identifying_close_blocks ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
cluster Segre_Product A : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(I : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) set ) : ( ( non empty ) ( non empty ) TopStruct ) -> non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ;
end;

theorem :: PENCIL_1:19
for T being ( ( ) ( ) TopStruct )
for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) is trivial holds
( S : ( ( ) ( ) Subset of ) is strong & S : ( ( ) ( ) Subset of ) is closed_under_lines ) ;

theorem :: PENCIL_1:20
for S being ( ( identifying_close_blocks ) ( identifying_close_blocks ) TopStruct )
for l being ( ( ) ( ) Block of S : ( ( identifying_close_blocks ) ( identifying_close_blocks ) TopStruct ) )
for L being ( ( ) ( ) Subset of ) st L : ( ( ) ( ) Subset of ) = l : ( ( ) ( ) Block of b1 : ( ( identifying_close_blocks ) ( identifying_close_blocks ) TopStruct ) ) holds
L : ( ( ) ( ) Subset of ) is closed_under_lines ;

theorem :: PENCIL_1:21
for S being ( ( ) ( ) TopStruct )
for l being ( ( ) ( ) Block of S : ( ( ) ( ) TopStruct ) )
for L being ( ( ) ( ) Subset of ) st L : ( ( ) ( ) Subset of ) = l : ( ( ) ( ) Block of b1 : ( ( ) ( ) TopStruct ) ) holds
L : ( ( ) ( ) Subset of ) is strong ;

theorem :: PENCIL_1:22
for S being ( ( non void ) ( non void ) TopStruct ) holds [#] S : ( ( non void ) ( non void ) TopStruct ) : ( ( ) ( non proper ) Element of bool the carrier of b1 : ( ( non void ) ( non void ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed_under_lines ;

theorem :: PENCIL_1:23
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for x, y being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st x : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) in product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty non trivial with_common_domain product-like ) set ) & y : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) in product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty non trivial with_common_domain product-like ) set ) holds
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) <> indx A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) holds
x : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) = y : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: PENCIL_1:24
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) Block of (Segre_Product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) TopStruct ) ) iff ex L being ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) st
( x : ( ( ) ( ) set ) = product L : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( functional non empty non trivial with_common_domain product-like ) set ) & L : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) . (indx L : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) is ( ( ) ( ) Block of (A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . (indx L : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) ( non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ) PLS) ) ) ) ;

theorem :: PENCIL_1:25
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for P being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st P : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds P : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) +* (i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: PENCIL_1:26
for I being ( ( non empty ) ( non empty ) set )
for A, B being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() finite cardinal countable V186() ext-real positive ) Element of NAT : ( ( ) ( non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) c= card ((product A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty non trivial with_common_domain product-like ) set ) /\ (product B : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty non trivial with_common_domain product-like ) set ) ) : ( ( ) ( ) set ) : ( ( cardinal ) ( V21() V22() V23() cardinal ) set ) holds
( indx A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = indx B : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) & ( for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) <> indx A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) holds
A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) = B : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: PENCIL_1:27
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for N being ( ( non trivial ) ( non empty non trivial ) set ) holds
( A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) +* ((indx A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) is Segre-like & not A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) +* ((indx A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,N : ( ( non trivial ) ( non empty non trivial ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) is trivial-yielding ) ;

theorem :: PENCIL_1:28
for S being ( ( non empty non void identifying_close_blocks without_isolated_points ) ( non empty non void identifying_close_blocks without_isolated_points ) TopStruct ) st S : ( ( non empty non void identifying_close_blocks without_isolated_points ) ( non empty non void identifying_close_blocks without_isolated_points ) TopStruct ) is strongly_connected holds
S : ( ( non empty non void identifying_close_blocks without_isolated_points ) ( non empty non void identifying_close_blocks without_isolated_points ) TopStruct ) is connected ;

theorem :: PENCIL_1:29
for I being ( ( non empty ) ( non empty ) set )
for A being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for S being ( ( ) ( ) Subset of ) holds
( ( not S : ( ( ) ( ) Subset of ) is trivial & S : ( ( ) ( ) Subset of ) is strong & S : ( ( ) ( ) Subset of ) is closed_under_lines ) iff ex B being ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier A : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) st
( S : ( ( ) ( ) Subset of ) = product B : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) : ( ( ) ( functional non empty non trivial with_common_domain product-like ) set ) & ( for C being ( ( ) ( ) Subset of ) st C : ( ( ) ( ) Subset of ) = B : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) . (indx B : ( ( non trivial-yielding Segre-like ) ( Relation-like V2() b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) non trivial-yielding Segre-like ) ManySortedSubset of Carrier b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) PLS-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) 1-sorted-yielding non-Empty TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V14(b1 : ( ( non empty ) ( non empty ) set ) ) ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
( C : ( ( ) ( ) Subset of ) is strong & C : ( ( ) ( ) Subset of ) is closed_under_lines ) ) ) ) ;