:: PENCIL_1 semantic presentation

theorem Th1: :: PENCIL_1:1
for b1, b2 being Function st product b1 = product b2 & b1 is non-empty holds
b2 is non-empty
proof end;

theorem Th2: :: PENCIL_1:2
for b1 being set holds
( 2 c= Card b1 iff ex b2, b3 being set st
( b2 in b1 & b3 in b1 & b2 <> b3 ) )
proof end;

theorem Th3: :: PENCIL_1:3
for b1 being set st 2 c= Card b1 holds
for b2 being set ex b3 being set st
( b3 in b1 & b2 <> b3 )
proof end;

theorem Th4: :: PENCIL_1:4
for b1 being set holds
( 2 c= Card b1 iff not b1 is trivial )
proof end;

theorem Th5: :: PENCIL_1:5
for b1 being set holds
( 3 c= Card b1 iff ex b2, b3, b4 being set st
( b2 in b1 & b3 in b1 & b4 in b1 & b2 <> b3 & b2 <> b4 & b3 <> b4 ) )
proof end;

theorem Th6: :: PENCIL_1:6
for b1 being set st 3 c= Card b1 holds
for b2, b3 being set ex b4 being set st
( b4 in b1 & b2 <> b4 & b3 <> b4 )
proof end;

definition
let c1 be TopStruct ;
mode Block of a1 is Element of the topology of a1;
end;

definition
let c1 be TopStruct ;
let c2, c3 be Point of c1;
pred c2,c3 are_collinear means :Def1: :: PENCIL_1:def 1
( a2 = a3 or ex b1 being Block of a1 st {a2,a3} c= b1 );
end;

:: deftheorem Def1 defines are_collinear PENCIL_1:def 1 :
for b1 being TopStruct
for b2, b3 being Point of b1 holds
( b2,b3 are_collinear iff ( b2 = b3 or ex b4 being Block of b1 st {b2,b3} c= b4 ) );

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
attr a2 is closed_under_lines means :Def2: :: PENCIL_1:def 2
for b1 being Block of a1 st 2 c= Card (b1 /\ a2) holds
b1 c= a2;
attr a2 is strong means :Def3: :: PENCIL_1:def 3
for b1, b2 being Point of a1 st b1 in a2 & b2 in a2 holds
b1,b2 are_collinear ;
end;

:: deftheorem Def2 defines closed_under_lines PENCIL_1:def 2 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is closed_under_lines iff for b3 being Block of b1 st 2 c= Card (b3 /\ b2) holds
b3 c= b2 );

:: deftheorem Def3 defines strong PENCIL_1:def 3 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is strong iff for b3, b4 being Point of b1 st b3 in b2 & b4 in b2 holds
b3,b4 are_collinear );

definition
let c1 be TopStruct ;
attr a1 is void means :Def4: :: PENCIL_1:def 4
the topology of a1 is empty;
attr a1 is degenerated means :Def5: :: PENCIL_1:def 5
the carrier of a1 is Block of a1;
attr a1 is with_non_trivial_blocks means :Def6: :: PENCIL_1:def 6
for b1 being Block of a1 holds 2 c= Card b1;
attr a1 is identifying_close_blocks means :Def7: :: PENCIL_1:def 7
for b1, b2 being Block of a1 st 2 c= Card (b1 /\ b2) holds
b1 = b2;
attr a1 is truly-partial means :Def8: :: PENCIL_1:def 8
not for b1, b2 being Point of a1 holds b1,b2 are_collinear ;
attr a1 is without_isolated_points means :Def9: :: PENCIL_1:def 9
for b1 being Point of a1 ex b2 being Block of a1 st b1 in b2;
attr a1 is connected means :: PENCIL_1:def 10
for b1, b2 being Point of a1 ex b3 being FinSequence of the carrier of a1 st
( b1 = b3 . 1 & b2 = b3 . (len b3) & ( for b4 being Nat st 1 <= b4 & b4 < len b3 holds
for b5, b6 being Point of a1 st b5 = b3 . b4 & b6 = b3 . (b4 + 1) holds
b5,b6 are_collinear ) );
attr a1 is strongly_connected means :Def11: :: PENCIL_1:def 11
for b1 being Point of a1
for b2 being Subset of a1 st b2 is closed_under_lines & b2 is strong holds
ex b3 being FinSequence of bool the carrier of a1 st
( b2 = b3 . 1 & b1 in b3 . (len b3) & ( for b4 being Subset of a1 st b4 in rng b3 holds
( b4 is closed_under_lines & b4 is strong ) ) & ( for b4 being Nat st 1 <= b4 & b4 < len b3 holds
2 c= Card ((b3 . b4) /\ (b3 . (b4 + 1))) ) );
end;

:: deftheorem Def4 defines void PENCIL_1:def 4 :
for b1 being TopStruct holds
( b1 is void iff the topology of b1 is empty );

:: deftheorem Def5 defines degenerated PENCIL_1:def 5 :
for b1 being TopStruct holds
( b1 is degenerated iff the carrier of b1 is Block of b1 );

:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def 6 :
for b1 being TopStruct holds
( b1 is with_non_trivial_blocks iff for b2 being Block of b1 holds 2 c= Card b2 );

:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def 7 :
for b1 being TopStruct holds
( b1 is identifying_close_blocks iff for b2, b3 being Block of b1 st 2 c= Card (b2 /\ b3) holds
b2 = b3 );

:: deftheorem Def8 defines truly-partial PENCIL_1:def 8 :
for b1 being TopStruct holds
( b1 is truly-partial iff not for b2, b3 being Point of b1 holds b2,b3 are_collinear );

:: deftheorem Def9 defines without_isolated_points PENCIL_1:def 9 :
for b1 being TopStruct holds
( b1 is without_isolated_points iff for b2 being Point of b1 ex b3 being Block of b1 st b2 in b3 );

:: deftheorem Def10 defines connected PENCIL_1:def 10 :
for b1 being TopStruct holds
( b1 is connected iff for b2, b3 being Point of b1 ex b4 being FinSequence of the carrier of b1 st
( b2 = b4 . 1 & b3 = b4 . (len b4) & ( for b5 being Nat st 1 <= b5 & b5 < len b4 holds
for b6, b7 being Point of b1 st b6 = b4 . b5 & b7 = b4 . (b5 + 1) holds
b6,b7 are_collinear ) ) );

:: deftheorem Def11 defines strongly_connected PENCIL_1:def 11 :
for b1 being TopStruct holds
( b1 is strongly_connected iff for b2 being Point of b1
for b3 being Subset of b1 st b3 is closed_under_lines & b3 is strong holds
ex b4 being FinSequence of bool the carrier of b1 st
( b3 = b4 . 1 & b2 in b4 . (len b4) & ( for b5 being Subset of b1 st b5 in rng b4 holds
( b5 is closed_under_lines & b5 is strong ) ) & ( for b5 being Nat st 1 <= b5 & b5 < len b4 holds
2 c= Card ((b4 . b5) /\ (b4 . (b5 + 1))) ) ) );

theorem Th7: :: PENCIL_1:7
for b1 being non empty set st 3 c= Card b1 holds
for b2 being TopStruct st the carrier of b2 = b1 & the topology of b2 = { b3 where B is Subset of b1 : 2 = Card b3 } holds
( not b2 is empty & not b2 is void & not b2 is degenerated & not b2 is truly-partial & b2 is with_non_trivial_blocks & b2 is identifying_close_blocks & b2 is without_isolated_points )
proof end;

Lemma18: ex b1 being TopStruct st
( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & not b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points )
proof end;

theorem Th8: :: PENCIL_1:8
for b1 being non empty set st 3 c= Card b1 holds
for b2 being Subset of b1 st Card b2 = 2 holds
for b3 being TopStruct st the carrier of b3 = b1 & the topology of b3 = { b4 where B is Subset of b1 : 2 = Card b4 } \ {b2} holds
( not b3 is empty & not b3 is void & not b3 is degenerated & b3 is truly-partial & b3 is with_non_trivial_blocks & b3 is identifying_close_blocks & b3 is without_isolated_points )
proof end;

Lemma20: ex b1 being TopStruct st
( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points )
proof end;

registration
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points TopStruct ;
existence
ex b1 being TopStruct st
( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & not b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points ) by Lemma18;
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points TopStruct ;
existence
ex b1 being TopStruct st
( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points ) by Lemma20;
end;

registration
let c1 be non void TopStruct ;
cluster the topology of a1 -> non empty ;
coherence
not the topology of c1 is empty by Def4;
end;

definition
let c1 be without_isolated_points TopStruct ;
let c2, c3 be Point of c1;
redefine pred c2,c3 are_collinear means :: PENCIL_1:def 12
ex b1 being Block of a1 st {a2,a3} c= b1;
compatibility
( c2,c3 are_collinear iff ex b1 being Block of c1 st {c2,c3} c= b1 )
proof end;
end;

:: deftheorem Def12 defines are_collinear PENCIL_1:def 12 :
for b1 being without_isolated_points TopStruct
for b2, b3 being Point of b1 holds
( b2,b3 are_collinear iff ex b4 being Block of b1 st {b2,b3} c= b4 );

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

definition
let c1 be Relation;
attr a1 is TopStruct-yielding means :Def13: :: PENCIL_1:def 13
for b1 being set st b1 in rng a1 holds
b1 is TopStruct ;
end;

:: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def 13 :
for b1 being Relation holds
( b1 is TopStruct-yielding iff for b2 being set st b2 in rng b1 holds
b2 is TopStruct );

registration
cluster TopStruct-yielding -> 1-sorted-yielding set ;
coherence
for b1 being Function st b1 is TopStruct-yielding holds
b1 is 1-sorted-yielding
proof end;
end;

registration
let c1 be set ;
cluster 1-sorted-yielding TopStruct-yielding ManySortedSet of a1;
existence
ex b1 being ManySortedSet of c1 st b1 is TopStruct-yielding
proof end;
end;

registration
cluster 1-sorted-yielding TopStruct-yielding set ;
existence
ex b1 being Function st b1 is TopStruct-yielding
proof end;
end;

definition
let c1 be Relation;
attr a1 is non-void-yielding means :Def14: :: PENCIL_1:def 14
for b1 being TopStruct st b1 in rng a1 holds
not b1 is void;
end;

:: deftheorem Def14 defines non-void-yielding PENCIL_1:def 14 :
for b1 being Relation holds
( b1 is non-void-yielding iff for b2 being TopStruct st b2 in rng b1 holds
not b2 is void );

definition
let c1 be TopStruct-yielding Function;
redefine attr a1 is non-void-yielding means :: PENCIL_1:def 15
for b1 being set st b1 in rng a1 holds
b1 is non void TopStruct ;
compatibility
( c1 is non-void-yielding iff for b1 being set st b1 in rng c1 holds
b1 is non void TopStruct )
proof end;
end;

:: deftheorem Def15 defines non-void-yielding PENCIL_1:def 15 :
for b1 being TopStruct-yielding Function holds
( b1 is non-void-yielding iff for b2 being set st b2 in rng b1 holds
b2 is non void TopStruct );

definition
let c1 be Relation;
attr a1 is trivial-yielding means :Def16: :: PENCIL_1:def 16
for b1 being set st b1 in rng a1 holds
b1 is trivial;
end;

:: deftheorem Def16 defines trivial-yielding PENCIL_1:def 16 :
for b1 being Relation holds
( b1 is trivial-yielding iff for b2 being set st b2 in rng b1 holds
b2 is trivial );

definition
let c1 be Relation;
attr a1 is non-Trivial-yielding means :Def17: :: PENCIL_1:def 17
for b1 being 1-sorted st b1 in rng a1 holds
not b1 is trivial;
end;

:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def 17 :
for b1 being Relation holds
( b1 is non-Trivial-yielding iff for b2 being 1-sorted st b2 in rng b1 holds
not b2 is trivial );

registration
cluster non-Trivial-yielding -> non-Empty set ;
coherence
for b1 being Relation st b1 is non-Trivial-yielding holds
b1 is non-Empty
proof end;
end;

definition
let c1 be 1-sorted-yielding Function;
redefine attr a1 is non-Trivial-yielding means :: PENCIL_1:def 18
for b1 being set st b1 in rng a1 holds
b1 is non trivial 1-sorted ;
compatibility
( c1 is non-Trivial-yielding iff for b1 being set st b1 in rng c1 holds
b1 is non trivial 1-sorted )
proof end;
end;

:: deftheorem Def18 defines non-Trivial-yielding PENCIL_1:def 18 :
for b1 being 1-sorted-yielding Function holds
( b1 is non-Trivial-yielding iff for b2 being set st b2 in rng b1 holds
b2 is non trivial 1-sorted );

definition
let c1 be non empty set ;
let c2 be TopStruct-yielding ManySortedSet of c1;
let c3 be Element of c1;
redefine func . as c2 . c3 -> TopStruct ;
coherence
c2 . c3 is TopStruct
proof end;
end;

definition
let c1 be Relation;
attr a1 is PLS-yielding means :Def19: :: PENCIL_1:def 19
for b1 being set st b1 in rng a1 holds
b1 is PLS;
end;

:: deftheorem Def19 defines PLS-yielding PENCIL_1:def 19 :
for b1 being Relation holds
( b1 is PLS-yielding iff for b2 being set st b2 in rng b1 holds
b2 is PLS );

registration
cluster PLS-yielding -> non-Empty 1-sorted-yielding TopStruct-yielding set ;
coherence
for b1 being Function st b1 is PLS-yielding holds
( b1 is non-Empty & b1 is TopStruct-yielding )
proof end;
cluster TopStruct-yielding PLS-yielding -> 1-sorted-yielding TopStruct-yielding non-void-yielding set ;
coherence
for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds
b1 is non-void-yielding
proof end;
cluster TopStruct-yielding PLS-yielding -> non-Empty 1-sorted-yielding TopStruct-yielding non-Trivial-yielding set ;
coherence
for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds
b1 is non-Trivial-yielding
proof end;
end;

registration
let c1 be set ;
cluster non-Empty 1-sorted-yielding TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ManySortedSet of a1;
existence
ex b1 being ManySortedSet of c1 st b1 is PLS-yielding
proof end;
end;

definition
let c1 be non empty set ;
let c2 be PLS-yielding ManySortedSet of c1;
let c3 be Element of c1;
redefine func . as c2 . c3 -> PLS;
coherence
c2 . c3 is PLS
proof end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
attr a2 is Segre-like means :Def20: :: PENCIL_1:def 20
ex b1 being Element of a1 st
for b2 being Element of a1 st b1 <> b2 holds
( not a2 . b2 is empty & a2 . b2 is trivial );
end;

:: deftheorem Def20 defines Segre-like PENCIL_1:def 20 :
for b1 being set
for b2 being ManySortedSet of b1 holds
( b2 is Segre-like iff ex b3 being Element of b1 st
for b4 being Element of b1 st b3 <> b4 holds
( not b2 . b4 is empty & b2 . b4 is trivial ) );

registration
let c1 be set ;
let c2 be ManySortedSet of c1;
cluster {a2} -> trivial-yielding ;
coherence
{c2} is trivial-yielding
proof end;
end;

theorem Th9: :: PENCIL_1:9
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being Element of b1
for b4 being non trivial set holds not b2 +* b3,b4 is trivial-yielding
proof end;

registration
let c1 be non empty set ;
let c2 be ManySortedSet of c1;
cluster {a2} -> trivial-yielding Segre-like ;
coherence
{c2} is Segre-like
proof end;
end;

theorem Th10: :: PENCIL_1:10
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3, b4 being set holds {b2} +* b3,b4 is Segre-like
proof end;

theorem Th11: :: PENCIL_1:11
for b1 being non empty set
for b2 being non-Empty 1-sorted-yielding ManySortedSet of b1
for b3 being Element of Carrier b2 holds {b3} is ManySortedSubset of Carrier b2
proof end;

registration
let c1 be non empty set ;
let c2 be non-Empty 1-sorted-yielding ManySortedSet of c1;
cluster V2 trivial-yielding Segre-like ManySortedSubset of Carrier a2;
existence
ex b1 being ManySortedSubset of Carrier c2 st
( b1 is Segre-like & b1 is trivial-yielding & b1 is non-empty )
proof end;
end;

registration
let c1 be non empty set ;
let c2 be 1-sorted-yielding non-Trivial-yielding ManySortedSet of c1;
cluster V2 non trivial-yielding Segre-like ManySortedSubset of Carrier a2;
existence
ex b1 being ManySortedSubset of Carrier c2 st
( b1 is Segre-like & not b1 is trivial-yielding & b1 is non-empty )
proof end;
end;

registration
let c1 be non empty set ;
cluster non trivial-yielding Segre-like ManySortedSet of a1;
existence
ex b1 being ManySortedSet of c1 st
( b1 is Segre-like & not b1 is trivial-yielding )
proof end;
end;

definition
let c1 be non empty set ;
let c2 be non trivial-yielding Segre-like ManySortedSet of c1;
func indx c2 -> Element of a1 means :Def21: :: PENCIL_1:def 21
not a2 . a3 is trivial;
existence
not for b1 being Element of c1 holds c2 . b1 is trivial
proof end;
uniqueness
for b1, b2 being Element of c1 st not c2 . b1 is trivial & not c2 . b2 is trivial holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines indx PENCIL_1:def 21 :
for b1 being non empty set
for b2 being non trivial-yielding Segre-like ManySortedSet of b1
for b3 being Element of b1 holds
( b3 = indx b2 iff not b2 . b3 is trivial );

theorem Th12: :: PENCIL_1:12
for b1 being non empty set
for b2 being non trivial-yielding Segre-like ManySortedSet of b1
for b3 being Element of b1 st b3 <> indx b2 holds
( not b2 . b3 is empty & b2 . b3 is trivial )
proof end;

registration
let c1 be non empty set ;
cluster non trivial-yielding Segre-like -> V2 ManySortedSet of a1;
coherence
for b1 being ManySortedSet of c1 st b1 is Segre-like & not b1 is trivial-yielding holds
b1 is non-empty
proof end;
end;

theorem Th13: :: PENCIL_1:13
for b1 being non empty set
for b2 being ManySortedSet of b1 holds
( 2 c= Card (product b2) iff ( b2 is non-empty & not b2 is trivial-yielding ) )
proof end;

registration
let c1 be non empty set ;
let c2 be non trivial-yielding Segre-like ManySortedSet of c1;
cluster product a2 -> non trivial ;
coherence
not product c2 is trivial
proof end;
end;

definition
let c1 be non empty set ;
let c2 be non-Empty TopStruct-yielding ManySortedSet of c1;
func Segre_Blocks c2 -> Subset-Family of (product (Carrier a2)) means :Def22: :: PENCIL_1:def 22
for b1 being set holds
( b1 in a3 iff ex b2 being Segre-like ManySortedSubset of Carrier a2 st
( b1 = product b2 & ex b3 being Element of a1 st b2 . b3 is Block of (a2 . b3) ) );
existence
ex b1 being Subset-Family of (product (Carrier c2)) st
for b2 being set holds
( b2 in b1 iff ex b3 being Segre-like ManySortedSubset of Carrier c2 st
( b2 = product b3 & ex b4 being Element of c1 st b3 . b4 is Block of (c2 . b4) ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (product (Carrier c2)) st ( for b3 being set holds
( b3 in b1 iff ex b4 being Segre-like ManySortedSubset of Carrier c2 st
( b3 = product b4 & ex b5 being Element of c1 st b4 . b5 is Block of (c2 . b5) ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being Segre-like ManySortedSubset of Carrier c2 st
( b3 = product b4 & ex b5 being Element of c1 st b4 . b5 is Block of (c2 . b5) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def 22 :
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1
for b3 being Subset-Family of (product (Carrier b2)) holds
( b3 = Segre_Blocks b2 iff for b4 being set holds
( b4 in b3 iff ex b5 being Segre-like ManySortedSubset of Carrier b2 st
( b4 = product b5 & ex b6 being Element of b1 st b5 . b6 is Block of (b2 . b6) ) ) );

definition
let c1 be non empty set ;
let c2 be non-Empty TopStruct-yielding ManySortedSet of c1;
func Segre_Product c2 -> non empty TopStruct equals :: PENCIL_1:def 23
 TopStruct(# (product (Carrier a2)),(Segre_Blocks a2) #);
correctness
coherence
TopStruct(# (product (Carrier c2)),(Segre_Blocks c2) #) is non empty TopStruct ;
by STRUCT_0:def 1;
end;

:: deftheorem Def23 defines Segre_Product PENCIL_1:def 23 :
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1 holds Segre_Product b2 = TopStruct(# (product (Carrier b2)),(Segre_Blocks b2) #);

theorem Th14: :: PENCIL_1:14
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1
for b3 being Point of (Segre_Product b2) holds b3 is ManySortedSet of b1
proof end;

theorem Th15: :: PENCIL_1:15
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1 st not for b3 being Element of b1 holds b2 . b3 is void holds
not Segre_Product b2 is void
proof end;

theorem Th16: :: PENCIL_1:16
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds
( not b2 . b3 is degenerated & not for b4 being Element of b1 holds b2 . b4 is void ) ) holds
not Segre_Product b2 is degenerated
proof end;

theorem Th17: :: PENCIL_1:17
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds
( b2 . b3 is with_non_trivial_blocks & not for b4 being Element of b1 holds b2 . b4 is void ) ) holds
Segre_Product b2 is with_non_trivial_blocks
proof end;

theorem Th18: :: PENCIL_1:18
for b1 being non empty set
for b2 being non-Empty TopStruct-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds
( b2 . b3 is identifying_close_blocks & b2 . b3 is with_non_trivial_blocks & not for b4 being Element of b1 holds b2 . b4 is void ) ) holds
Segre_Product b2 is identifying_close_blocks
proof end;

definition
let c1 be non empty set ;
let c2 be PLS-yielding ManySortedSet of c1;
redefine func Segre_Product as Segre_Product c2 -> PLS;
coherence
Segre_Product c2 is PLS
proof end;
end;

theorem Th19: :: PENCIL_1:19
for b1 being TopStruct
for b2 being Subset of b1 st b2 is trivial holds
( b2 is strong & b2 is closed_under_lines )
proof end;

theorem Th20: :: PENCIL_1:20
for b1 being identifying_close_blocks TopStruct
for b2 being Block of b1
for b3 being Subset of b1 st b3 = b2 holds
b3 is closed_under_lines
proof end;

theorem Th21: :: PENCIL_1:21
for b1 being TopStruct
for b2 being Block of b1
for b3 being Subset of b1 st b3 = b2 holds
b3 is strong
proof end;

theorem Th22: :: PENCIL_1:22
for b1 being non void TopStruct holds [#] b1 is closed_under_lines
proof end;

theorem Th23: :: PENCIL_1:23
for b1 being non empty set
for b2 being non trivial-yielding Segre-like ManySortedSet of b1
for b3, b4 being ManySortedSet of b1 st b3 in product b2 & b4 in product b2 holds
for b5 being set st b5 <> indx b2 holds
b3 . b5 = b4 . b5
proof end;

theorem Th24: :: PENCIL_1:24
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1
for b3 being set holds
( b3 is Block of (Segre_Product b2) iff ex b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier b2 st
( b3 = product b4 & b4 . (indx b4) is Block of (b2 . (indx b4)) ) )
proof end;

theorem Th25: :: PENCIL_1:25
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1
for b3 being ManySortedSet of b1 st b3 is Point of (Segre_Product b2) holds
for b4 being Element of b1
for b5 being Point of (b2 . b4) holds b3 +* b4,b5 is Point of (Segre_Product b2)
proof end;

theorem Th26: :: PENCIL_1:26
for b1 being non empty set
for b2, b3 being non trivial-yielding Segre-like ManySortedSet of b1 st 2 c= Card ((product b2) /\ (product b3)) holds
( indx b2 = indx b3 & ( for b4 being set st b4 <> indx b2 holds
b2 . b4 = b3 . b4 ) )
proof end;

theorem Th27: :: PENCIL_1:27
for b1 being non empty set
for b2 being non trivial-yielding Segre-like ManySortedSet of b1
for b3 being non trivial set holds
( b2 +* (indx b2),b3 is Segre-like & not b2 +* (indx b2),b3 is trivial-yielding )
proof end;

theorem Th28: :: PENCIL_1:28
for b1 being non empty non void identifying_close_blocks without_isolated_points TopStruct st b1 is strongly_connected holds
b1 is connected
proof end;

theorem Th29: :: PENCIL_1:29
for b1 being non empty set
for b2 being PLS-yielding ManySortedSet of b1
for b3 being Subset of (Segre_Product b2) holds
( ( not b3 is trivial & b3 is strong & b3 is closed_under_lines ) iff ex b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier b2 st
( b3 = product b4 & ( for b5 being Subset of (b2 . (indx b4)) st b5 = b4 . (indx b4) holds
( b5 is strong & b5 is closed_under_lines ) ) ) )
proof end;