:: PENCIL_1 semantic presentation

begin

theorem Th1: :: PENCIL_1:1
for f, g being Function st product f = product g & f is non-empty holds
g is non-empty
proof
let f, g be Function; ::_thesis: ( product f = product g & f is non-empty implies g is non-empty )
assume A1: product f = product g ; ::_thesis: ( not f is non-empty or g is non-empty )
now__::_thesis:_(_f_is_non-empty_implies_g_is_non-empty_)
assume that
A2: f is non-empty and
A3: not g is non-empty ; ::_thesis: contradiction
 ex n being set st
( n in dom g & g . n is empty ) by A3, FUNCT_1:def_9;
then  {} in rng g by FUNCT_1:def_3;
then  product g = {} by CARD_3:26;
then  {} in rng f by A1, CARD_3:26;
then  ex n being set st
( n in dom f & f . n = {} ) by FUNCT_1:def_3;
hence  contradiction by A2, FUNCT_1:def_9; ::_thesis: verum
end;
hence  ( not f is non-empty or g is non-empty ) ; ::_thesis: verum
end;

theorem Th2: :: PENCIL_1:2
for X being set holds
( 2 c= card X iff ex x, y being set st
( x in X & y in X & x <> y ) )
proof
let X be set ; ::_thesis: ( 2 c= card X iff ex x, y being set st
( x in X & y in X & x <> y ) )
thus  ( 2 c= card X implies ex x, y being set st
( x in X & y in X & x <> y ) ) ::_thesis: ( ex x, y being set st
( x in X & y in X & x <> y ) implies 2 c= card X )
proof
assume  2 c= card X ; ::_thesis: ex x, y being set st
( x in X & y in X & x <> y )
then  card 2 c= card X by CARD_1:def_2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = 2 and
A3: rng f c= X by CARD_1:10;
take x = f . 0; ::_thesis: ex y being set st
( x in X & y in X & x <> y )
take y = f . 1; ::_thesis: ( x in X & y in X & x <> y )
A4: 0 in dom f by A2, CARD_1:50, TARSKI:def_2;
then  f . 0 in rng f by FUNCT_1:def_3;
hence  x in X by A3; ::_thesis: ( y in X & x <> y )
A5: 1 in dom f by A2, CARD_1:50, TARSKI:def_2;
then  f . 1 in rng f by FUNCT_1:def_3;
hence  y in X by A3; ::_thesis: x <> y
thus  x <> y by A1, A4, A5, FUNCT_1:def_4; ::_thesis: verum
end;
given x, y being set  such that A6: ( x in X & y in X ) and
A7: x <> y ; ::_thesis: 2 c= card X
 {x,y} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in X )
assume  a in {x,y} ; ::_thesis: a in X
hence  a in X by A6, TARSKI:def_2; ::_thesis: verum
end;
then  card {x,y} c= card X by CARD_1:11;
hence  2 c= card X by A7, CARD_2:57; ::_thesis: verum
end;

theorem Th3: :: PENCIL_1:3
for X being set st 2 c= card X holds
for x being set ex y being set st
( y in X & x <> y )
proof
let X be set ; ::_thesis: ( 2 c= card X implies for x being set ex y being set st
( y in X & x <> y ) )
assume  2 c= card X ; ::_thesis: for x being set ex y being set st
( y in X & x <> y )
then consider a, b being set  such that
A1: a in X and
A2: ( b in X & a <> b ) by Th2;
let x be set ; ::_thesis: ex y being set st
( y in X & x <> y )
percases ( x = a or x <> a ) ;
supposeA3: x = a ; ::_thesis: ex y being set st
( y in X & x <> y )
take  b ; ::_thesis: ( b in X & x <> b )
thus  ( b in X & x <> b ) by A2, A3; ::_thesis: verum
end;
supposeA4: x <> a ; ::_thesis: ex y being set st
( y in X & x <> y )
take  a ; ::_thesis: ( a in X & x <> a )
thus  ( a in X & x <> a ) by A1, A4; ::_thesis: verum
end;
end;
end;

theorem Th4: :: PENCIL_1:4
for X being set holds
( 2 c= card X iff not X is trivial )
proof
let X be set ; ::_thesis: ( 2 c= card X iff not X is trivial )
set z = the Element of X;
thus  ( 2 c= card X implies not X is trivial ) ::_thesis: ( not X is trivial implies 2 c= card X )
proof
assume  2 c= card X ; ::_thesis: not X is trivial
then consider x, y being set  such that
A1: x in X and
A2: y in X and
A3: x <> y by Th2;
now__::_thesis:_(_ex_z_being_set_st_X_=_{z}_implies_x_=_y_)
given z being set  such that A4: X = {z} ; ::_thesis: x = y
thus x = z by A1, A4, TARSKI:def_1
.= y by A2, A4, TARSKI:def_1 ; ::_thesis: verum
end;
hence  not X is trivial by A1, A3, ZFMISC_1:131; ::_thesis: verum
end;
assume A5: not X is trivial ; ::_thesis: 2 c= card X
then  ( X c= { the Element of X} implies X = { the Element of X} ) ;
then consider w being set  such that
A6: w in X and
A7: not w in { the Element of X} by A5, TARSKI:def_3;
 w <> the Element of X by A7, TARSKI:def_1;
hence  2 c= card X by A6, Th2; ::_thesis: verum
end;

theorem Th5: :: PENCIL_1:5
for X being set holds
( 3 c= card X iff ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
proof
let X be set ; ::_thesis: ( 3 c= card X iff ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
thus  ( 3 c= card X implies ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) ) ::_thesis: ( ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) implies 3 c= card X )
proof
assume  3 c= card X ; ::_thesis: ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
then  card 3 c= card X by CARD_1:def_2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = 3 and
A3: rng f c= X by CARD_1:10;
take x = f . 0; ::_thesis: ex y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
take y = f . 1; ::_thesis: ex z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
take z = f . 2; ::_thesis: ( x in X & y in X & z in X & x <> y & x <> z & y <> z )
A4: 0 in dom f by A2, ENUMSET1:def_1, YELLOW11:1;
then  f . 0 in rng f by FUNCT_1:def_3;
hence  x in X by A3; ::_thesis: ( y in X & z in X & x <> y & x <> z & y <> z )
A5: 1 in dom f by A2, ENUMSET1:def_1, YELLOW11:1;
then  f . 1 in rng f by FUNCT_1:def_3;
hence  y in X by A3; ::_thesis: ( z in X & x <> y & x <> z & y <> z )
A6: 2 in dom f by A2, ENUMSET1:def_1, YELLOW11:1;
then  f . 2 in rng f by FUNCT_1:def_3;
hence  z in X by A3; ::_thesis: ( x <> y & x <> z & y <> z )
thus  x <> y by A1, A4, A5, FUNCT_1:def_4; ::_thesis: ( x <> z & y <> z )
thus  x <> z by A1, A4, A6, FUNCT_1:def_4; ::_thesis: y <> z
thus  y <> z by A1, A5, A6, FUNCT_1:def_4; ::_thesis: verum
end;
given x, y, z being set  such that A7: ( x in X & y in X & z in X ) and
A8: ( x <> y & x <> z & y <> z ) ; ::_thesis: 3 c= card X
 {x,y,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y,z} or a in X )
assume  a in {x,y,z} ; ::_thesis: a in X
hence  a in X by A7, ENUMSET1:def_1; ::_thesis: verum
end;
then  card {x,y,z} c= card X by CARD_1:11;
hence  3 c= card X by A8, CARD_2:58; ::_thesis: verum
end;

theorem Th6: :: PENCIL_1:6
for X being set st 3 c= card X holds
for x, y being set ex z being set st
( z in X & x <> z & y <> z )
proof
let X be set ; ::_thesis: ( 3 c= card X implies for x, y being set ex z being set st
( z in X & x <> z & y <> z ) )
assume  3 c= card X ; ::_thesis: for x, y being set ex z being set st
( z in X & x <> z & y <> z )
then consider a, b, c being set  such that
A1: a in X and
A2: b in X and
A3: c in X and
A4: a <> b and
A5: ( a <> c & b <> c ) by Th5;
let x, y be set ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
percases ( ( x <> a & y <> a ) or ( x <> a & y = a & x = b ) or ( x <> a & y = a & x <> b ) or ( x = a & y <> a & y = b ) or ( x = a & y <> a & y <> b ) or ( x = a & y = a ) ) ;
suppose ( x <> a & y <> a ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence  ex z being set st
( z in X & x <> z & y <> z ) by A1; ::_thesis: verum
end;
suppose ( x <> a & y = a & x = b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence  ex z being set st
( z in X & x <> z & y <> z ) by A3, A5; ::_thesis: verum
end;
suppose ( x <> a & y = a & x <> b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence  ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; ::_thesis: verum
end;
suppose ( x = a & y <> a & y = b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence  ex z being set st
( z in X & x <> z & y <> z ) by A3, A5; ::_thesis: verum
end;
suppose ( x = a & y <> a & y <> b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence  ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; ::_thesis: verum
end;
suppose ( x = a & y = a ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence  ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; ::_thesis: verum
end;
end;
end;

begin

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

definition
let S be TopStruct ;
let x, y be Point of S;
predx,y are_collinear  means :Def1: :: PENCIL_1:def 1
( x = y or ex l being Block of S st {x,y} c= l );
end;

:: deftheorem Def1 defines are_collinear PENCIL_1:def_1_:_
 for S being TopStruct
for x, y being Point of S holds
( x,y are_collinear iff ( x = y or ex l being Block of S st {x,y} c= l ) );

definition
let S be TopStruct ;
let T be Subset of S;
attrT is closed_under_lines  means :Def2: :: PENCIL_1:def 2
 for l being Block of S st 2 c= card (l /\ T) holds
l c= T;
attrT is strong  means :Def3: :: PENCIL_1:def 3
 for x, y being Point of S st x in T & y in T holds
x,y are_collinear ;
end;

:: deftheorem Def2 defines closed_under_lines PENCIL_1:def_2_:_
 for S being TopStruct
for T being Subset of S holds
( T is closed_under_lines iff for l being Block of S st 2 c= card (l /\ T) holds
l c= T );

:: deftheorem Def3 defines strong PENCIL_1:def_3_:_
 for S being TopStruct
for T being Subset of S holds
( T is strong iff for x, y being Point of S st x in T & y in T holds
x,y are_collinear );

definition
let S be TopStruct ;
attrS is void  means :Def4: :: PENCIL_1:def 4
 the topology of S is empty ;
attrS is degenerated  means :Def5: :: PENCIL_1:def 5
 the carrier of S is Block of S;
attrS is with_non_trivial_blocks  means :Def6: :: PENCIL_1:def 6
 for k being Block of S holds 2 c= card k;
attrS is identifying_close_blocks  means :Def7: :: PENCIL_1:def 7
 for k, l being Block of S st 2 c= card (k /\ l) holds
k = l;
attrS is truly-partial  means :Def8: :: PENCIL_1:def 8
 not for x, y being Point of S holds x,y are_collinear ;
attrS is without_isolated_points  means :Def9: :: PENCIL_1:def 9
 for x being Point of S ex l being Block of S st x in l;
attrS is connected  means :: PENCIL_1:def 10
 for x, y being Point of S ex f being FinSequence of the carrier of S st
( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) );
attrS is strongly_connected  means :Def11: :: PENCIL_1:def 11
 for x being Point of S
for X being Subset of S st X is closed_under_lines & X is strong holds
ex f being FinSequence of bool the carrier of S st
( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) );
end;

:: deftheorem Def4 defines void PENCIL_1:def_4_:_
 for S being TopStruct holds
( S is void iff the topology of S is empty );

:: deftheorem Def5 defines degenerated PENCIL_1:def_5_:_
 for S being TopStruct holds
( S is degenerated iff the carrier of S is Block of S );

:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def_6_:_
 for S being TopStruct holds
( S is with_non_trivial_blocks iff for k being Block of S holds 2 c= card k );

:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def_7_:_
 for S being TopStruct holds
( S is identifying_close_blocks iff for k, l being Block of S st 2 c= card (k /\ l) holds
k = l );

:: deftheorem Def8 defines truly-partial PENCIL_1:def_8_:_
 for S being TopStruct holds
( S is truly-partial iff not for x, y being Point of S holds x,y are_collinear );

:: deftheorem Def9 defines without_isolated_points PENCIL_1:def_9_:_
 for S being TopStruct holds
( S is without_isolated_points iff for x being Point of S ex l being Block of S st x in l );

:: deftheorem  defines connected PENCIL_1:def_10_:_
 for S being TopStruct holds
( S is connected iff for x, y being Point of S ex f being FinSequence of the carrier of S st
( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) ) );

:: deftheorem Def11 defines strongly_connected PENCIL_1:def_11_:_
 for S being TopStruct holds
( S is strongly_connected iff for x being Point of S
for X being Subset of S st X is closed_under_lines & X is strong holds
ex f being FinSequence of bool the carrier of S st
( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) ) );

theorem Th7: :: PENCIL_1:7
for X being non empty set st 3 c= card X holds
for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  holds
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
let X be non empty set ; ::_thesis: ( 3 c= card X implies for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  holds
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A1: 3 c= card X ; ::_thesis: for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  holds
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
A2: 2 c= 3 by NAT_1:39;
then  2 c= card X by A1, XBOOLE_1:1;
then consider x, y being set  such that
A3: ( x in X & y in X ) and
A4: x <> y by Th2;
 {x,y} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in X )
assume  a in {x,y} ; ::_thesis: a in X
hence  a in X by A3, TARSKI:def_2; ::_thesis: verum
end;
then reconsider l = {x,y} as Subset of X ;
let S be TopStruct ; ::_thesis: ( the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  implies ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume that
A5: the carrier of S = X and
A6: the topology of S =  {  L where L is Subset of X : 2 = card L  }  ; ::_thesis: ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus  not S is empty by A5; ::_thesis: ( not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
 2 = card l by A4, CARD_2:57;
then A7: l in the topology of S by A6;
then reconsider F =  {  L where L is Subset of X : 2 = card L  }  as non empty set by A6;
thus  not S is void by A7, Def4; ::_thesis: ( not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
now__::_thesis:_not_X_in_F
assume  X in F ; ::_thesis: contradiction
then  ex L being Subset of X st
( X = L & 2 = card L ) ;
hence  contradiction by A1, NAT_1:39; ::_thesis: verum
end;
then  X is not Element of F ;
hence  not S is degenerated by A5, A6, Def5; ::_thesis: ( not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
 for x, y being Point of S holds x,y are_collinear
proof
let x, y be Point of S; ::_thesis: x,y are_collinear
percases ( x = y or x <> y ) ;
supposeA8: x = y ; ::_thesis: x,y are_collinear
consider z being set  such that
A9: z in X and
A10: z <> x by A1, A2, Th3, XBOOLE_1:1;
reconsider z = z as Point of S by A5, A9;
A11: {x,y} c= {x,z}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in {x,z} )
assume  a in {x,y} ; ::_thesis: a in {x,z}
then  ( a = x or a = y ) by TARSKI:def_2;
hence  a in {x,z} by A8, TARSKI:def_2; ::_thesis: verum
end;
 {x,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,z} or a in X )
assume  a in {x,z} ; ::_thesis: a in X
then  ( a = x or a = z ) by TARSKI:def_2;
hence  a in X by A5; ::_thesis: verum
end;
then reconsider l = {x,z} as Subset of X ;
 card l = 2 by A10, CARD_2:57;
then  l in the topology of S by A6;
hence  x,y are_collinear by A11, Def1; ::_thesis: verum
end;
supposeA12: x <> y ; ::_thesis: x,y are_collinear
 {x,y} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in X )
assume  a in {x,y} ; ::_thesis: a in X
then  ( a = x or a = y ) by TARSKI:def_2;
hence  a in X by A5; ::_thesis: verum
end;
then reconsider l = {x,y} as Subset of X ;
 card {x,y} = 2 by A12, CARD_2:57;
then  l in the topology of S by A6;
hence  x,y are_collinear by Def1; ::_thesis: verum
end;
end;
end;
hence  not S is truly-partial by Def8; ::_thesis: ( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus  S is with_non_trivial_blocks ::_thesis: ( S is identifying_close_blocks & S is without_isolated_points )
proof
let k be Block of S; :: according to PENCIL_1:def_6 ::_thesis: 2 c= card k
 k in the topology of S by A7;
then  ex m being Subset of X st
( m = k & card m = 2 ) by A6;
hence  2 c= card k ; ::_thesis: verum
end;
thus  S is identifying_close_blocks ::_thesis: S is without_isolated_points
proof
let k, l be Block of S; :: according to PENCIL_1:def_7 ::_thesis: ( 2 c= card (k /\ l) implies k = l )
assume  2 c= card (k /\ l) ; ::_thesis: k = l
then consider a, b being set  such that
A13: ( a in k /\ l & b in k /\ l ) and
A14: a <> b by Th2;
A15: {a,b} c= k /\ l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in k /\ l )
assume  x in {a,b} ; ::_thesis: x in k /\ l
hence  x in k /\ l by A13, TARSKI:def_2; ::_thesis: verum
end;
 l in the topology of S by A7;
then A16: ex n being Subset of X st
( n = l & card n = 2 ) by A6;
then reconsider l1 = l as finite set ;
A17: k /\ l c= l1 by XBOOLE_1:17;
 k in the topology of S by A7;
then A18: ex m being Subset of X st
( m = k & card m = 2 ) by A6;
then reconsider k1 = k as finite set ;
A19: card {a,b} = 2 by A14, CARD_2:57;
 k /\ l c= k1 by XBOOLE_1:17;
then  {a,b} = k1 by A18, A15, A19, PRE_POLY:8, XBOOLE_1:1;
hence  k = l by A15, A19, A16, A17, PRE_POLY:8, XBOOLE_1:1; ::_thesis: verum
end;
thus  S is without_isolated_points ::_thesis: verum
proof
let x be Point of S; :: according to PENCIL_1:def_9 ::_thesis: ex l being Block of S st x in l
consider z being set  such that
A20: z in X and
A21: z <> x by A1, A2, Th3, XBOOLE_1:1;
 {x,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,z} or a in X )
assume  a in {x,z} ; ::_thesis: a in X
then  ( a = x or a = z ) by TARSKI:def_2;
hence  a in X by A5, A20; ::_thesis: verum
end;
then reconsider l = {x,z} as Subset of X ;
 card {x,z} = 2 by A21, CARD_2:57;
then  l in the topology of S by A6;
then reconsider l = l as Block of S ;
take  l ; ::_thesis: x in l
thus  x in l by TARSKI:def_2; ::_thesis: verum
end;
end;

theorem Th8: :: PENCIL_1:8
for X being non empty set st 3 c= card X holds
for K being Subset of X st card K = 2 holds
for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
let X be non empty set ; ::_thesis: ( 3 c= card X implies for K being Subset of X st card K = 2 holds
for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A1: 3 c= card X ; ::_thesis: for K being Subset of X st card K = 2 holds
for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
let K be Subset of X; ::_thesis: ( card K = 2 implies for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A2: card K = 2 ; ::_thesis: for S being TopStruct st the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} holds
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
then reconsider K9 = K as finite Subset of X ;
consider x, y being set  such that
A3: x <> y and
A4: K9 = {x,y} by A2, CARD_2:60;
let S be TopStruct ; ::_thesis: ( the carrier of S = X & the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} implies ( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume that
A5: the carrier of S = X and
A6: the topology of S =  {  L where L is Subset of X : 2 = card L  }  \ {K} ; ::_thesis: ( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
reconsider x = x, y = y as Point of S by A5, A4, ZFMISC_1:32;
consider z being set  such that
A7: z in X and
A8: z <> x and
A9: z <> y by A1, Th6;
 {x,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,z} or a in X )
assume  a in {x,z} ; ::_thesis: a in X
then  ( a = x or a = z ) by TARSKI:def_2;
hence  a in X by A5, A7; ::_thesis: verum
end;
then reconsider l = {x,z} as Subset of X ;
 card l = 2 by A8, CARD_2:57;
then A10: ( z in l & l in  {  L where L is Subset of X : 2 = card L  }  ) by TARSKI:def_2;
thus  not S is empty by A5; ::_thesis: ( not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
 not z in K9 by A4, A8, A9, TARSKI:def_2;
then A11: not  {  L where L is Subset of X : 2 = card L  }  c= {K} by A10, TARSKI:def_1;
then A12: not  {  L where L is Subset of X : 2 = card L  }  \ {K} is empty by XBOOLE_1:37;
hence  not S is void by A6, Def4; ::_thesis: ( not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
reconsider F =  {  L where L is Subset of X : 2 = card L  }  \ {K} as non empty set by A11, XBOOLE_1:37;
now__::_thesis:_not_X_in_F
assume  X in F ; ::_thesis: contradiction
then  X in  {  L where L is Subset of X : 2 = card L  }  ;
then  ex L being Subset of X st
( X = L & 2 = card L ) ;
hence  contradiction by A1, NAT_1:39; ::_thesis: verum
end;
then  X is not Element of F ;
hence  not S is degenerated by A5, A6, Def5; ::_thesis: ( S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus  S is truly-partial ::_thesis: ( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
take  x ; :: according to PENCIL_1:def_8 ::_thesis: not for y being Point of S holds x,y are_collinear
take  y ; ::_thesis: not x,y are_collinear
 for l being Block of S holds not {x,y} c= l
proof
let l be Block of S; ::_thesis: not {x,y} c= l
 l in  {  L where L is Subset of X : 2 = card L  }  by A6, A12, XBOOLE_0:def_5;
then consider L being Subset of X such that
A13: l = L and
A14: card L = 2 ;
reconsider L9 = L as finite Subset of X by A14;
consider a, b being set  such that
 a <> b and
A15: L9 = {a,b} by A14, CARD_2:60;
A16: not l in {K} by A6, A12, XBOOLE_0:def_5;
now__::_thesis:_not_{x,y}_c=_l
assume A17: {x,y} c= l ; ::_thesis: contradiction
then  y in L9 by A13, ZFMISC_1:32;
then A18: ( y = a or y = b ) by A15, TARSKI:def_2;
 x in L9 by A13, A17, ZFMISC_1:32;
then  ( x = a or x = b ) by A15, TARSKI:def_2;
hence  contradiction by A3, A4, A16, A13, A15, A18, TARSKI:def_1; ::_thesis: verum
end;
hence  not {x,y} c= l ; ::_thesis: verum
end;
hence  not x,y are_collinear by A3, Def1; ::_thesis: verum
end;
thus  S is with_non_trivial_blocks ::_thesis: ( S is identifying_close_blocks & S is without_isolated_points )
proof
let k be Block of S; :: according to PENCIL_1:def_6 ::_thesis: 2 c= card k
 k in  {  L where L is Subset of X : 2 = card L  }  by A6, A12, XBOOLE_0:def_5;
then  ex m being Subset of X st
( m = k & card m = 2 ) ;
hence  2 c= card k ; ::_thesis: verum
end;
thus  S is identifying_close_blocks ::_thesis: S is without_isolated_points
proof
let k, l be Block of S; :: according to PENCIL_1:def_7 ::_thesis: ( 2 c= card (k /\ l) implies k = l )
assume  2 c= card (k /\ l) ; ::_thesis: k = l
then consider a, b being set  such that
A19: ( a in k /\ l & b in k /\ l ) and
A20: a <> b by Th2;
A21: {a,b} c= k /\ l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in k /\ l )
assume  x in {a,b} ; ::_thesis: x in k /\ l
hence  x in k /\ l by A19, TARSKI:def_2; ::_thesis: verum
end;
 l in  {  L where L is Subset of X : 2 = card L  }  by A6, A12, XBOOLE_0:def_5;
then A22: ex n being Subset of X st
( n = l & card n = 2 ) ;
then reconsider l1 = l as finite set ;
A23: k /\ l c= l1 by XBOOLE_1:17;
 k in  {  L where L is Subset of X : 2 = card L  }  by A6, A12, XBOOLE_0:def_5;
then A24: ex m being Subset of X st
( m = k & card m = 2 ) ;
then reconsider k1 = k as finite set ;
A25: card {a,b} = 2 by A20, CARD_2:57;
 k /\ l c= k1 by XBOOLE_1:17;
then  {a,b} = k1 by A24, A21, A25, PRE_POLY:8, XBOOLE_1:1;
hence  k = l by A21, A25, A22, A23, PRE_POLY:8, XBOOLE_1:1; ::_thesis: verum
end;
A26: 2 c= 3 by NAT_1:39;
thus  S is without_isolated_points ::_thesis: verum
proof
let p be Point of S; :: according to PENCIL_1:def_9 ::_thesis: ex l being Block of S st p in l
percases ( ( p <> x & p <> y ) or p = x or p = y ) ;
supposeA27: ( p <> x & p <> y ) ; ::_thesis: ex l being Block of S st p in l
consider z being set  such that
A28: z in X and
A29: z <> p by A1, A26, Th3, XBOOLE_1:1;
 {p,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {p,z} or a in X )
assume  a in {p,z} ; ::_thesis: a in X
then  ( a = p or a = z ) by TARSKI:def_2;
hence  a in X by A5, A28; ::_thesis: verum
end;
then reconsider el = {p,z} as Subset of X ;
 card {p,z} = 2 by A29, CARD_2:57;
then A30: el in  {  L where L is Subset of X : 2 = card L  }  ;
 p in el by TARSKI:def_2;
then  el <> K by A4, A27, TARSKI:def_2;
then  not el in {K} by TARSKI:def_1;
then reconsider el = el as Block of S by A6, A30, XBOOLE_0:def_5;
take  el ; ::_thesis: p in el
thus  p in el by TARSKI:def_2; ::_thesis: verum
end;
supposeA31: ( p = x or p = y ) ; ::_thesis: ex l being Block of S st p in l
consider z being set  such that
A32: z in X and
A33: ( z <> x & z <> y ) by A1, Th6;
 {p,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {p,z} or a in X )
assume  a in {p,z} ; ::_thesis: a in X
then  ( a = p or a = z ) by TARSKI:def_2;
hence  a in X by A5, A32; ::_thesis: verum
end;
then reconsider el = {p,z} as Subset of X ;
 card {p,z} = 2 by A31, A33, CARD_2:57;
then A34: el in  {  L where L is Subset of X : 2 = card L  }  ;
 z in el by TARSKI:def_2;
then  el <> K by A4, A33, TARSKI:def_2;
then  not el in {K} by TARSKI:def_1;
then reconsider el = el as Block of S by A6, A34, XBOOLE_0:def_5;
take  el ; ::_thesis: p in el
thus  p in el by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
end;

registration
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points for 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 )
proof
  {  L where L is Subset of 3 : 2 = card L  }  c= bool 3
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  L where L is Subset of 3 : 2 = card L  }  or x in bool 3 )
assume  x in  {  L where L is Subset of 3 : 2 = card L  }  ; ::_thesis: x in bool 3
then  ex L being Subset of 3 st
( x = L & 2 = card L ) ;
hence  x in bool 3 ; ::_thesis: verum
end;
then reconsider B =  {  L where L is Subset of 3 : 2 = card L  }  as Subset-Family of 3 ;
take  TopStruct(# 3,B #) ; ::_thesis: ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & not TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points )
 3 = card 3 by CARD_1:def_2;
hence  ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & not TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points ) by Th7; ::_thesis: verum
end;
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points for 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 )
proof
 ( 2 c= 3 & card 2 = 2 ) by CARD_1:def_2, NAT_1:39;
then consider K being Subset of 3 such that
A1: card K = 2 ;
  {  L where L is Subset of 3 : 2 = card L  }  c= bool 3
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  L where L is Subset of 3 : 2 = card L  }  or x in bool 3 )
assume  x in  {  L where L is Subset of 3 : 2 = card L  }  ; ::_thesis: x in bool 3
then  ex L being Subset of 3 st
( x = L & 2 = card L ) ;
hence  x in bool 3 ; ::_thesis: verum
end;
then reconsider B =  {  L where L is Subset of 3 : 2 = card L  }  \ {K} as Subset-Family of 3 by XBOOLE_1:1;
take  TopStruct(# 3,B #) ; ::_thesis: ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points )
 3 c= card 3 by CARD_1:def_2;
hence  ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points ) by A1, Th8; ::_thesis: verum
end;
end;

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

definition
let S be without_isolated_points TopStruct ;
let x, y be Point of S;
redefine pred x,y are_collinear  means :: PENCIL_1:def 12
 ex l being Block of S st {x,y} c= l;
compatibility
 ( x,y are_collinear iff ex l being Block of S st {x,y} c= l )
proof
thus  ( x,y are_collinear implies ex l being Block of S st {x,y} c= l ) ::_thesis: ( ex l being Block of S st {x,y} c= l implies x,y are_collinear )
proof
assume A1: x,y are_collinear ; ::_thesis: ex l being Block of S st {x,y} c= l
percases ( x = y or x <> y ) ;
supposeA2: x = y ; ::_thesis: ex l being Block of S st {x,y} c= l
consider l being Block of S such that
A3: x in l by Def9;
take  l ; ::_thesis: {x,y} c= l
thus  {x,y} c= l by A2, A3, ZFMISC_1:32; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: ex l being Block of S st {x,y} c= l
hence  ex l being Block of S st {x,y} c= l by A1, Def1; ::_thesis: verum
end;
end;
end;
given l being Block of S such that A4: {x,y} c= l ; ::_thesis: x,y are_collinear
thus  x,y are_collinear by A4, Def1; ::_thesis: verum
end;
end;

:: deftheorem  defines are_collinear PENCIL_1:def_12_:_
 for S being without_isolated_points TopStruct
for x, y being Point of S holds
( x,y are_collinear iff ex l being Block of S st {x,y} c= l );

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

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

:: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def_13_:_
 for F being Relation holds
( F is TopStruct-yielding iff for x being set st x in rng F holds
x is TopStruct );

registration
cluster Relation-like Function-like TopStruct-yielding  ->  1-sorted-yielding for set ;
coherence
 for b1 being Function st b1 is TopStruct-yielding holds
b1 is 1-sorted-yielding
proof
let F be Function; ::_thesis: ( F is TopStruct-yielding implies F is 1-sorted-yielding )
assume A1: F is TopStruct-yielding ; ::_thesis: F is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom F or F . x is 1-sorted )
assume  x in dom F ; ::_thesis: F . x is 1-sorted
then  F . x in rng F by FUNCT_1:def_3;
hence  F . x is 1-sorted by A1, Def13; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) TopStruct-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is TopStruct-yielding
proof
set R = the TopStruct ;
take  I --> the TopStruct ; ::_thesis: I --> the TopStruct is TopStruct-yielding
let v be set ; :: according to PENCIL_1:def_13 ::_thesis: ( v in rng (I --> the TopStruct ) implies v is TopStruct )
assume A1: v in rng (I --> the TopStruct ) ; ::_thesis: v is TopStruct
 rng (I --> the TopStruct ) c= { the TopStruct } by FUNCOP_1:13;
hence  v is TopStruct by A1, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like TopStruct-yielding for set ;
existence
 ex b1 being Function st b1 is TopStruct-yielding
proof
set F = the TopStruct-yielding ManySortedSet of {} ;
take  the TopStruct-yielding ManySortedSet of {} ; ::_thesis: the TopStruct-yielding ManySortedSet of {} is TopStruct-yielding
thus  the TopStruct-yielding ManySortedSet of {} is TopStruct-yielding ; ::_thesis: verum
end;
end;

definition
let F be Relation;
attrF is non-void-yielding  means :Def14: :: PENCIL_1:def 14
 for S being TopStruct st S in rng F holds
not S is void ;
end;

:: deftheorem Def14 defines non-void-yielding PENCIL_1:def_14_:_
 for F being Relation holds
( F is non-void-yielding iff for S being TopStruct st S in rng F holds
not S is void );

definition
let F be TopStruct-yielding Function;
redefine attr F is non-void-yielding  means :: PENCIL_1:def 15
 for i being set st i in rng F holds
i is non void TopStruct ;
compatibility
 ( F is non-void-yielding iff for i being set st i in rng F holds
i is non void TopStruct )
proof
thus  ( F is non-void-yielding implies for i being set st i in rng F holds
i is non void TopStruct ) by Def13, Def14; ::_thesis: ( ( for i being set st i in rng F holds
i is non void TopStruct ) implies F is non-void-yielding )
assume A1: for i being set st i in rng F holds
i is non void TopStruct ; ::_thesis: F is non-void-yielding
let S be TopStruct ; :: according to PENCIL_1:def_14 ::_thesis: ( S in rng F implies not S is void )
thus  ( S in rng F implies not S is void ) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines non-void-yielding PENCIL_1:def_15_:_
 for F being TopStruct-yielding Function holds
( F is non-void-yielding iff for i being set st i in rng F holds
i is non void TopStruct );

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

:: deftheorem Def16 defines trivial-yielding PENCIL_1:def_16_:_
 for F being Relation holds
( F is trivial-yielding iff for S being set st S in rng F holds
S is trivial );

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

:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def_17_:_
 for F being Relation holds
( F is non-Trivial-yielding iff for S being 1-sorted st S in rng F holds
not S is trivial );

registration
cluster Relation-like non-Trivial-yielding  ->  non-Empty for set ;
coherence
 for b1 being Relation st b1 is non-Trivial-yielding holds
b1 is non-Empty
proof
let F be Relation; ::_thesis: ( F is non-Trivial-yielding implies F is non-Empty )
assume A1: F is non-Trivial-yielding ; ::_thesis: F is non-Empty
let i be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not i in rng F or not i is empty )
assume  i in rng F ; ::_thesis: not i is empty
hence  not i is empty by A1, Def17; ::_thesis: verum
end;
end;

definition
let F be 1-sorted-yielding Function;
redefine attr F is non-Trivial-yielding  means :: PENCIL_1:def 18
 for i being set st i in rng F holds
i is non trivial 1-sorted ;
compatibility
 ( F is non-Trivial-yielding iff for i being set st i in rng F holds
i is non trivial 1-sorted )
proof
hereby  ::_thesis: ( ( for i being set st i in rng F holds
i is non trivial 1-sorted ) implies F is non-Trivial-yielding )
assume A1: F is non-Trivial-yielding ; ::_thesis: for i being set st i in rng F holds
i is non trivial 1-sorted
let i be set ; ::_thesis: ( i in rng F implies i is non trivial 1-sorted )
assume A2: i in rng F ; ::_thesis: i is non trivial 1-sorted
then  ex x being set st
( x in dom F & i = F . x ) by FUNCT_1:def_3;
hence  i is non trivial 1-sorted by A1, A2, Def17, PRALG_1:def_11; ::_thesis: verum
end;
assume A3: for i being set st i in rng F holds
i is non trivial 1-sorted ; ::_thesis: F is non-Trivial-yielding
let S be 1-sorted ; :: according to PENCIL_1:def_17 ::_thesis: ( S in rng F implies not S is trivial )
thus  ( S in rng F implies not S is trivial ) by A3; ::_thesis: verum
end;
end;

:: deftheorem  defines non-Trivial-yielding PENCIL_1:def_18_:_
 for F being 1-sorted-yielding Function holds
( F is non-Trivial-yielding iff for i being set st i in rng F holds
i is non trivial 1-sorted );

definition
let I be non empty set ;
let A be TopStruct-yielding ManySortedSet of I;
let j be Element of I;
:: original: .
redefine funcA . j ->  TopStruct ;
coherence
 A . j is TopStruct
proof
 dom A = I by PARTFUN1:def_2;
then  A . j in rng A by FUNCT_1:def_3;
hence  A . j is TopStruct by Def13; ::_thesis: verum
end;
end;

definition
let F be Relation;
attrF is PLS-yielding  means :Def19: :: PENCIL_1:def 19
 for x being set st x in rng F holds
x is PLS;
end;

:: deftheorem Def19 defines PLS-yielding PENCIL_1:def_19_:_
 for F being Relation holds
( F is PLS-yielding iff for x being set st x in rng F holds
x is PLS );

registration
cluster Relation-like Function-like PLS-yielding  ->  non-Empty TopStruct-yielding for set ;
coherence
 for b1 being Function st b1 is PLS-yielding holds
( b1 is non-Empty & b1 is TopStruct-yielding )
proof
let f be Function; ::_thesis: ( f is PLS-yielding implies ( f is non-Empty & f is TopStruct-yielding ) )
assume A1: f is PLS-yielding ; ::_thesis: ( f is non-Empty & f is TopStruct-yielding )
thus  f is non-Empty ::_thesis: f is TopStruct-yielding
proof
let S be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not S in rng f or not S is empty )
assume  S in rng f ; ::_thesis: not S is empty
hence  not S is empty by A1, Def19; ::_thesis: verum
end;
let x be set ; :: according to PENCIL_1:def_13 ::_thesis: ( x in rng f implies x is TopStruct )
assume  x in rng f ; ::_thesis: x is TopStruct
hence  x is TopStruct by A1, Def19; ::_thesis: verum
end;
cluster Relation-like Function-like TopStruct-yielding PLS-yielding  ->  TopStruct-yielding non-void-yielding for set ;
coherence
 for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds
b1 is non-void-yielding
proof
let f be TopStruct-yielding Function; ::_thesis: ( f is PLS-yielding implies f is non-void-yielding )
assume A2: f is PLS-yielding ; ::_thesis: f is non-void-yielding
let x be set ; :: according to PENCIL_1:def_15 ::_thesis: ( x in rng f implies x is non void TopStruct )
assume  x in rng f ; ::_thesis: x is non void TopStruct
hence  x is non void TopStruct by A2, Def19; ::_thesis: verum
end;
cluster Relation-like Function-like TopStruct-yielding PLS-yielding  ->  TopStruct-yielding non-Trivial-yielding for set ;
coherence
 for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds
b1 is non-Trivial-yielding
proof
let f be TopStruct-yielding Function; ::_thesis: ( f is PLS-yielding implies f is non-Trivial-yielding )
assume A3: f is PLS-yielding ; ::_thesis: f is non-Trivial-yielding
let x be set ; :: according to PENCIL_1:def_18 ::_thesis: ( x in rng f implies x is non trivial 1-sorted )
assume  x in rng f ; ::_thesis: x is non trivial 1-sorted
then reconsider S1 = x as non empty non void with_non_trivial_blocks TopStruct by A3, Def19;
consider s being set  such that
A4: s in the topology of S1 by XBOOLE_0:def_1;
reconsider s = s as Block of S1 by A4;
 2 c= card s by Def6;
then  ex s1, s2 being set st
( s1 in s & s2 in s & s1 <> s2 ) by Th2;
hence  x is non trivial 1-sorted by A4, STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) PLS-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is PLS-yielding
proof
set R = the PLS;
take  I --> the PLS ; ::_thesis: I --> the PLS is PLS-yielding
let v be set ; :: according to PENCIL_1:def_19 ::_thesis: ( v in rng (I --> the PLS) implies v is PLS )
assume A1: v in rng (I --> the PLS) ; ::_thesis: v is PLS
 rng (I --> the PLS) c= { the PLS} by FUNCOP_1:13;
hence  v is PLS by A1, TARSKI:def_1; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
let j be Element of I;
:: original: .
redefine funcA . j ->  PLS;
coherence
 A . j is PLS
proof
 dom A = I by PARTFUN1:def_2;
then  A . j in rng A by FUNCT_1:def_3;
hence  A . j is PLS by Def19; ::_thesis: verum
end;
end;

definition
let I be set ;
let A be ManySortedSet of I;
attrA is Segre-like  means :Def20: :: PENCIL_1:def 20
 ex i being Element of I st
for j being Element of I st i <> j holds
A . j is 1 -element ;
end;

:: deftheorem Def20 defines Segre-like PENCIL_1:def_20_:_
 for I being set
for A being ManySortedSet of I holds
( A is Segre-like iff ex i being Element of I st
for j being Element of I st i <> j holds
A . j is 1 -element );

registration
let I be set ;
let A be ManySortedSet of I;
cluster{A} ->  trivial-yielding ;
coherence
 {A} is trivial-yielding
proof
let a be set ; :: according to PENCIL_1:def_16 ::_thesis: ( a in rng {A} implies a is trivial )
assume  a in rng {A} ; ::_thesis: a is trivial
then consider i being set  such that
A1: ( i in dom {A} & a = {A} . i ) by FUNCT_1:def_3;
 dom {A} = I by PARTFUN1:def_2;
then  a = {(A . i)} by A1, PZFMISC1:def_1;
hence  a is trivial ; ::_thesis: verum
end;
end;

theorem :: PENCIL_1:9
for I being non empty set
for A being ManySortedSet of I
for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I
for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
let A be ManySortedSet of I; ::_thesis: for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
let i be Element of I; ::_thesis: for S being non trivial set holds not A +* (i,S) is trivial-yielding
let S be non trivial set ; ::_thesis: not A +* (i,S) is trivial-yielding
take a = (A +* (i,S)) . i; :: according to PENCIL_1:def_16 ::_thesis: ( a in rng (A +* (i,S)) & not a is trivial )
 dom A = I by PARTFUN1:def_2;
then  i in dom A ;
then  i in dom (A +* (i,S)) by FUNCT_7:30;
hence  a in rng (A +* (i,S)) by FUNCT_1:def_3; ::_thesis: not a is trivial
 dom A = I by PARTFUN1:def_2;
hence  not a is trivial by FUNCT_7:31; ::_thesis: verum
end;

registration
let I be non empty set ;
let A be ManySortedSet of I;
cluster{A} ->  Segre-like ;
coherence
 {A} is Segre-like
proof
set i = the Element of I;
take  the Element of I ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st the Element of I <> j holds
{A} . j is 1 -element
let j be Element of I; ::_thesis: ( the Element of I <> j implies {A} . j is 1 -element )
assume  the Element of I <> j ; ::_thesis: {A} . j is 1 -element
 {A} . j = {(A . j)} by PZFMISC1:def_1;
hence  {A} . j is 1 -element ; ::_thesis: verum
end;
end;

theorem :: PENCIL_1:10
for I being non empty set
for A being ManySortedSet of I
for i, S being set holds {A} +* (i,S) is Segre-like
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I
for i, S being set holds {A} +* (i,S) is Segre-like
let A be ManySortedSet of I; ::_thesis: for i, S being set holds {A} +* (i,S) is Segre-like
let i, S be set ; ::_thesis: {A} +* (i,S) is Segre-like
percases ( not i in I or i in I ) ;
suppose not i in I ; ::_thesis: {A} +* (i,S) is Segre-like
then  not i in dom {A} by PARTFUN1:def_2;
hence  {A} +* (i,S) is Segre-like by FUNCT_7:def_3; ::_thesis: verum
end;
suppose i in I ; ::_thesis: {A} +* (i,S) is Segre-like
then reconsider i = i as Element of I ;
take  i ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st i <> j holds
({A} +* (i,S)) . j is 1 -element
let j be Element of I; ::_thesis: ( i <> j implies ({A} +* (i,S)) . j is 1 -element )
assume A1: i <> j ; ::_thesis: ({A} +* (i,S)) . j is 1 -element
 {A} . j = {(A . j)} by PZFMISC1:def_1;
hence  ({A} +* (i,S)) . j is 1 -element by A1, FUNCT_7:32; ::_thesis: verum
end;
end;
end;

theorem Th11: :: PENCIL_1:11
for I being non empty set
for A being 1-sorted-yielding non-Empty ManySortedSet of I
for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
proof
let I be non empty set ; ::_thesis: for A being 1-sorted-yielding non-Empty ManySortedSet of I
for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
let A be 1-sorted-yielding non-Empty ManySortedSet of I; ::_thesis: for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
let B be Element of Carrier A; ::_thesis: {B} is ManySortedSubset of Carrier A
 {B} c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {B} . i c= (Carrier A) . i )
assume A1: i in I ; ::_thesis: {B} . i c= (Carrier A) . i
then reconsider j = i as Element of I ;
 j in dom A by A1, PARTFUN1:def_2;
then  A . j in rng A by FUNCT_1:def_3;
then A2: not A . j is empty by YELLOW_6:def_2;
 B . j is Element of (Carrier A) . j by PBOOLE:def_14;
then  B . j is Element of (A . j) by YELLOW_6:2;
then  {(B . j)} c= the carrier of (A . j) by A2, ZFMISC_1:31;
then  {B} . j c= the carrier of (A . j) by PZFMISC1:def_1;
hence  {B} . i c= (Carrier A) . i by YELLOW_6:2; ::_thesis: verum
end;
hence  {B} is ManySortedSubset of Carrier A by PBOOLE:def_18; ::_thesis: verum
end;

registration
let I be non empty set ;
let A be 1-sorted-yielding non-Empty ManySortedSet of I;
cluster Relation-like V2() I -defined Function-like V14(I) trivial-yielding Segre-like for ManySortedSubset of Carrier A;
existence
 ex b1 being ManySortedSubset of Carrier A st
( b1 is Segre-like & b1 is trivial-yielding & b1 is V2() )
proof
set B = the Element of Carrier A;
reconsider C = { the Element of Carrier A} as ManySortedSubset of Carrier A by Th11;
take  C ; ::_thesis: ( C is Segre-like & C is trivial-yielding & C is V2() )
thus  ( C is Segre-like & C is trivial-yielding & C is V2() ) ; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I;
cluster Relation-like V2() I -defined Function-like V14(I) non trivial-yielding Segre-like for ManySortedSubset of Carrier A;
existence
 ex b1 being ManySortedSubset of Carrier A st
( b1 is Segre-like & not b1 is trivial-yielding & b1 is V2() )
proof
set B = the Element of Carrier A;
set i1 = the Element of I;
A1: ex R being 1-sorted st
( R = A . the Element of I & the carrier of R = (Carrier A) . the Element of I ) by PRALG_1:def_13;
then reconsider b1 = the Element of Carrier A . the Element of I as Element of (A . the Element of I) by PBOOLE:def_14;
reconsider B = the Element of Carrier A as ManySortedSet of I ;
 dom A = I by PARTFUN1:def_2;
then  A . the Element of I in rng A by FUNCT_1:def_3;
then  not A . the Element of I is trivial by Def17;
then reconsider Ai1 = the carrier of (A . the Element of I) as non trivial set ;
 ex x1, x2 being Element of Ai1 st x1 <> x2 by SUBSET_1:def_7;
then  2 c= card the carrier of (A . the Element of I) by Th2;
then consider b2 being set  such that
A2: b2 in the carrier of (A . the Element of I) and
A3: b1 <> b2 by Th3;
reconsider b2 = b2 as Element of (A . the Element of I) by A2;
set B1 = B +* ( the Element of I,b2);
A4: for i being set st i in I holds
(B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
proof
let i be set ; ::_thesis: ( i in I implies (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i )
assume A5: i in I ; ::_thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
percases ( i <> the Element of I or i = the Element of I ) ;
suppose i <> the Element of I ; ::_thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
then  (B +* ( the Element of I,b2)) . i = B . i by FUNCT_7:32;
hence  (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i by A5, PBOOLE:def_14; ::_thesis: verum
end;
supposeA6: i = the Element of I ; ::_thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
then  the Element of I in dom B by A5, PARTFUN1:def_2;
hence  (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i by A1, A6, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
 {B,(B +* ( the Element of I,b2))} c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i )
assume A7: i in I ; ::_thesis: {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i
then reconsider j = i as Element of I ;
 j in dom A by A7, PARTFUN1:def_2;
then  A . j in rng A by FUNCT_1:def_3;
then A8: not A . j is empty by YELLOW_6:def_2;
 B . j is Element of (Carrier A) . j by PBOOLE:def_14;
then A9: B . j is Element of (A . j) by YELLOW_6:2;
 (B +* ( the Element of I,b2)) . j is Element of (Carrier A) . j by A4;
then  (B +* ( the Element of I,b2)) . j is Element of (A . j) by YELLOW_6:2;
then  {(B . j),((B +* ( the Element of I,b2)) . j)} c= the carrier of (A . j) by A8, A9, ZFMISC_1:32;
then  {B,(B +* ( the Element of I,b2))} . j c= the carrier of (A . j) by PZFMISC1:def_2;
hence  {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i by YELLOW_6:2; ::_thesis: verum
end;
then reconsider C = {B,(B +* ( the Element of I,b2))} as ManySortedSubset of Carrier A by PBOOLE:def_18;
 dom B = I by PARTFUN1:def_2;
then  (B +* ( the Element of I,b2)) . the Element of I = b2 by FUNCT_7:31;
then A10: C . the Element of I = {b1,b2} by PZFMISC1:def_2;
A11: now__::_thesis:_not_C_._the_Element_of_I_is_trivial
assume  C . the Element of I is trivial ; ::_thesis: contradiction
then  ( C . the Element of I is empty or ex x being set st C . the Element of I = {x} ) by ZFMISC_1:131;
hence  contradiction by A3, A10, ZFMISC_1:5; ::_thesis: verum
end;
take  C ; ::_thesis: ( C is Segre-like & not C is trivial-yielding & C is V2() )
thus  C is Segre-like ::_thesis: ( not C is trivial-yielding & C is V2() )
proof
take  the Element of I ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st the Element of I <> j holds
C . j is 1 -element
let j be Element of I; ::_thesis: ( the Element of I <> j implies C . j is 1 -element )
assume  the Element of I <> j ; ::_thesis: C . j is 1 -element
then  B . j = (B +* ( the Element of I,b2)) . j by FUNCT_7:32;
then C . j = {(B . j),(B . j)} by PZFMISC1:def_2
.= {(B . j)} by ENUMSET1:29 ;
hence  C . j is 1 -element ; ::_thesis: verum
end;
 dom C = I by PARTFUN1:def_2;
then  C . the Element of I in rng C by FUNCT_1:def_3;
hence  not C is trivial-yielding by A11, Def16; ::_thesis: C is V2()
thus  C is V2() ; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is Segre-like & not b1 is trivial-yielding )
proof
set B = the ManySortedSet of I;
set i = the Element of I;
take C = { the ManySortedSet of I} +* ( the Element of I,{0,1}); ::_thesis: ( C is Segre-like & not C is trivial-yielding )
thus  C is Segre-like ::_thesis: not C is trivial-yielding
proof
take  the Element of I ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st the Element of I <> j holds
C . j is 1 -element
let j be Element of I; ::_thesis: ( the Element of I <> j implies C . j is 1 -element )
assume  j <> the Element of I ; ::_thesis: C . j is 1 -element
then A1: C . j = { the ManySortedSet of I} . j by FUNCT_7:32;
 j in I ;
then A2: j in dom { the ManySortedSet of I} by PARTFUN1:def_2;
then  C . j in rng { the ManySortedSet of I} by A1, FUNCT_1:def_3;
then  ( not C . j is empty & C . j is trivial ) by A2, A1, Def16, FUNCT_1:def_9;
hence  C . j is 1 -element ; ::_thesis: verum
end;
thus  not C is trivial-yielding ::_thesis: verum
proof
take S = C . the Element of I; :: according to PENCIL_1:def_16 ::_thesis: ( S in rng C & not S is trivial )
 dom C = I by PARTFUN1:def_2;
hence  S in rng C by FUNCT_1:def_3; ::_thesis: not S is trivial
 dom { the ManySortedSet of I} = I by PARTFUN1:def_2;
then A3: C . the Element of I = {0,1} by FUNCT_7:31;
 ( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def_2;
then  2 c= card {0,1} by Th2;
hence  not S is trivial by A3, Th4; ::_thesis: verum
end;
end;
end;

definition
let I be non empty set ;
let B be non trivial-yielding Segre-like ManySortedSet of I;
func indx B ->  Element of I means :Def21: :: PENCIL_1:def 21
 not B . it is trivial ;
existence
 not  for b1 being Element of I holds B . b1 is trivial
proof
consider i being Element of I such that
A1: for j being Element of I st i <> j holds
B . j is 1 -element by Def20;
take  i ; ::_thesis: not B . i is trivial
now__::_thesis:_not_B_._i_is_trivial
assume A2: B . i is trivial ; ::_thesis: contradiction
 for S being set st S in rng B holds
S is trivial
proof
let S be set ; ::_thesis: ( S in rng B implies S is trivial )
assume  S in rng B ; ::_thesis: S is trivial
then consider j being set  such that
A3: j in dom B and
A4: S = B . j by FUNCT_1:def_3;
reconsider j = j as Element of I by A3, PARTFUN1:def_2;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: S is trivial
hence  S is trivial by A2, A4; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: S is trivial
then  B . j is 1 -element by A1;
hence  S is trivial by A4; ::_thesis: verum
end;
end;
end;
hence  contradiction by Def16; ::_thesis: verum
end;
hence  not B . i is trivial ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of I st not B . b1 is trivial & not B . b2 is trivial holds
b1 = b2
proof
let i1, i2 be Element of I; ::_thesis: ( not B . i1 is trivial & not B . i2 is trivial implies i1 = i2 )
assume that
A5: not B . i1 is trivial and
A6: not B . i2 is trivial ; ::_thesis: i1 = i2
consider i being Element of I such that
A7: for j being Element of I st i <> j holds
B . j is 1 -element by Def20;
A8: not B . i2 is 1 -element by A6;
 not B . i1 is 1 -element by A5;
hence i1 = i by A7
.= i2 by A7, A8 ;
::_thesis: verum
end;
end;

:: deftheorem Def21 defines indx PENCIL_1:def_21_:_
 for I being non empty set
for B being non trivial-yielding Segre-like ManySortedSet of I
for b3 being Element of I holds
( b3 = indx B iff not B . b3 is trivial );

theorem Th12: :: PENCIL_1:12
for I being non empty set
for A being non trivial-yielding Segre-like ManySortedSet of I
for i being Element of I st i <> indx A holds
A . i is 1 -element
proof
let I be non empty set ; ::_thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for i being Element of I st i <> indx A holds
A . i is 1 -element
let A be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: for i being Element of I st i <> indx A holds
A . i is 1 -element
let i be Element of I; ::_thesis: ( i <> indx A implies A . i is 1 -element )
consider j being Element of I such that
A1: for k being Element of I st k <> j holds
A . k is 1 -element by Def20;
A2: now__::_thesis:_not_indx_A_<>_j
assume  indx A <> j ; ::_thesis: contradiction
then  A . (indx A) is 1 -element by A1;
hence  contradiction by Def21; ::_thesis: verum
end;
assume  i <> indx A ; ::_thesis: A . i is 1 -element
hence  A . i is 1 -element by A1, A2; ::_thesis: verum
end;

registration
let I be non empty set ;
cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like  -> V2() for set ;
coherence
 for b1 being ManySortedSet of I st b1 is Segre-like & not b1 is trivial-yielding holds
b1 is V2()
proof
let f be ManySortedSet of I; ::_thesis: ( f is Segre-like & not f is trivial-yielding implies f is V2() )
assume  ( f is Segre-like & not f is trivial-yielding ) ; ::_thesis: f is V2()
then reconsider g = f as non trivial-yielding Segre-like ManySortedSet of I ;
now__::_thesis:_not_{}_in_rng_g
assume  {} in rng g ; ::_thesis: contradiction
then consider i being set  such that
A1: i in dom f and
A2: g . i = {} by FUNCT_1:def_3;
reconsider i = i as Element of I by A1, PARTFUN1:def_2;
percases ( i = indx g or i <> indx g ) ;
suppose i = indx g ; ::_thesis: contradiction
hence  contradiction by A2, Def21; ::_thesis: verum
end;
suppose i <> indx g ; ::_thesis: contradiction
then  g . i is 1 -element by Th12;
hence  contradiction by A2; ::_thesis: verum
end;
end;
end;
hence  f is V2() by RELAT_1:def_9; ::_thesis: verum
end;
end;

theorem Th13: :: PENCIL_1:13
for I being non empty set
for A being ManySortedSet of I holds
( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I holds
( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )
let A be ManySortedSet of I; ::_thesis: ( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )
A1: dom A = I by PARTFUN1:def_2;
thus  ( 2 c= card (product A) implies ( A is V2() & not A is trivial-yielding ) ) ::_thesis: ( A is V2() & not A is trivial-yielding implies 2 c= card (product A) )
proof
assume  2 c= card (product A) ; ::_thesis: ( A is V2() & not A is trivial-yielding )
then consider a, b being set  such that
A2: a in product A and
A3: b in product A and
A4: a <> b by Th2;
consider a1 being Function such that
A5: ( a = a1 & dom a1 = dom A ) and
A6: for e being set st e in dom A holds
a1 . e in A . e by A2, CARD_3:def_5;
thus  A is V2() ::_thesis: not A is trivial-yielding
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not A . i is empty )
assume  i in I ; ::_thesis: not A . i is empty
hence  not A . i is empty by A1, A6; ::_thesis: verum
end;
consider b1 being Function such that
A7: ( b = b1 & dom b1 = dom A ) and
A8: for e being set st e in dom A holds
b1 . e in A . e by A3, CARD_3:def_5;
consider e being set  such that
A9: e in dom A and
A10: b1 . e <> a1 . e by A4, A5, A7, FUNCT_1:2;
thus  not A is trivial-yielding ::_thesis: verum
proof
take  A . e ; :: according to PENCIL_1:def_16 ::_thesis: ( A . e in rng A & not A . e is trivial )
thus  A . e in rng A by A9, FUNCT_1:def_3; ::_thesis: not A . e is trivial
 ( a1 . e in A . e & b1 . e in A . e ) by A6, A8, A9;
then  2 c= card (A . e) by A10, Th2;
hence  not A . e is trivial by Th4; ::_thesis: verum
end;
end;
assume A11: ( A is V2() & not A is trivial-yielding ) ; ::_thesis: 2 c= card (product A)
then consider r being set  such that
A12: r in rng A and
A13: not r is trivial by Def16;
now__::_thesis:_not_{}_in_rng_A
assume  {} in rng A ; ::_thesis: contradiction
then  ex o being set st
( o in dom A & A . o = {} ) by FUNCT_1:def_3;
hence  contradiction by A1, A11, PBOOLE:def_13; ::_thesis: verum
end;
then  not product A is empty by CARD_3:26;
then consider a1 being set  such that
A14: a1 in product A by XBOOLE_0:def_1;
consider p being set  such that
A15: p in dom A and
A16: r = A . p by A12, FUNCT_1:def_3;
consider a being Function such that
A17: a = a1 and
A18: dom a = dom A and
A19: for o being set st o in dom A holds
a . o in A . o by A14, CARD_3:def_5;
reconsider a = a as ManySortedSet of I by A1, A18, PARTFUN1:def_2, RELAT_1:def_18;
 2 c= card r by A13, Th4;
then consider t being set  such that
A20: t in r and
A21: t <> a . p by Th3;
reconsider p = p as Element of I by A15, PARTFUN1:def_2;
set b = a +* (p,t);
A22: now__::_thesis:_for_o_being_set_st_o_in_dom_A_holds_
(a_+*_(p,t))_._o_in_A_._o
let o be set ; ::_thesis: ( o in dom A implies (a +* (p,t)) . b1 in A . b1 )
assume A23: o in dom A ; ::_thesis: (a +* (p,t)) . b1 in A . b1
percases ( o <> p or o = p ) ;
suppose o <> p ; ::_thesis: (a +* (p,t)) . b1 in A . b1
then  (a +* (p,t)) . o = a . o by FUNCT_7:32;
hence  (a +* (p,t)) . o in A . o by A19, A23; ::_thesis: verum
end;
suppose o = p ; ::_thesis: (a +* (p,t)) . b1 in A . b1
hence  (a +* (p,t)) . o in A . o by A18, A15, A16, A20, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
dom (a +* (p,t)) = I by PARTFUN1:def_2
.= dom A by PARTFUN1:def_2 ;
then A24: a +* (p,t) in product A by A22, CARD_3:9;
 (a +* (p,t)) . p = t by A18, A15, FUNCT_7:31;
hence  2 c= card (product A) by A14, A17, A21, A24, Th2; ::_thesis: verum
end;

registration
let I be non empty set ;
let B be non trivial-yielding Segre-like ManySortedSet of I;
cluster product B ->  non trivial ;
coherence
 not product B is trivial
proof
consider f being set  such that
A1: f in product B by XBOOLE_0:def_1;
A2: ex g being Function st
( g = f & dom g = dom B & ( for x being set st x in dom B holds
g . x in B . x ) ) by A1, CARD_3:def_5;
 dom B = I by PARTFUN1:def_2;
then reconsider f = f as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
 not B . (indx B) is trivial by Def21;
then  2 c= card (B . (indx B)) by Th4;
then consider y being set  such that
A3: y in B . (indx B) and
A4: y <> f . (indx B) by Th3;
set l = f +* ((indx B),y);
A5: for x being set st x in dom B holds
(f +* ((indx B),y)) . x in B . x
proof
let x be set ; ::_thesis: ( x in dom B implies (f +* ((indx B),y)) . x in B . x )
assume A6: x in dom B ; ::_thesis: (f +* ((indx B),y)) . x in B . x
then  x in I by PARTFUN1:def_2;
then A7: x in dom f by PARTFUN1:def_2;
percases ( x = indx B or x <> indx B ) ;
suppose x = indx B ; ::_thesis: (f +* ((indx B),y)) . x in B . x
hence  (f +* ((indx B),y)) . x in B . x by A3, A7, FUNCT_7:31; ::_thesis: verum
end;
suppose x <> indx B ; ::_thesis: (f +* ((indx B),y)) . x in B . x
then  (f +* ((indx B),y)) . x = f . x by FUNCT_7:32;
hence  (f +* ((indx B),y)) . x in B . x by A2, A6; ::_thesis: verum
end;
end;
end;
 dom f = I by PARTFUN1:def_2;
then A8: (f +* ((indx B),y)) . (indx B) = y by FUNCT_7:31;
dom (f +* ((indx B),y)) = I by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
then  f +* ((indx B),y) in product B by A5, CARD_3:def_5;
then  2 c= card (product B) by A1, A4, A8, Th2;
hence  not product B is trivial by Th4; ::_thesis: verum
end;
end;

begin

definition
let I be non empty set ;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
func Segre_Blocks A ->  Subset-Family of (product (Carrier A)) means :Def22: :: PENCIL_1:def 22
 for x being set holds
( x in it iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) );
existence
 ex b1 being Subset-Family of (product (Carrier A)) st
for x being set holds
( x in b1 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )
proof
defpred S1[ set ] means  ex B being Segre-like ManySortedSubset of Carrier A st
( $1 = product B & ex i being Element of I st B . i is Block of (A . i) );
consider S being set  such that
A1: for x being set holds
( x in S iff ( x in bool (product (Carrier A)) & S1[x] ) ) from XBOOLE_0:sch_1();
 S c= bool (product (Carrier A))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S or a in bool (product (Carrier A)) )
assume  a in S ; ::_thesis: a in bool (product (Carrier A))
hence  a in bool (product (Carrier A)) by A1; ::_thesis: verum
end;
then reconsider S = S as Subset-Family of (product (Carrier A)) ;
take  S ; ::_thesis: for x being set holds
( x in S iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )
let x be set ; ::_thesis: ( x in S iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )
thus  ( x in S implies ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) by A1; ::_thesis: ( ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) implies x in S )
given B being Segre-like ManySortedSubset of Carrier A such that A2: x = product B and
A3: ex i being Element of I st B . i is Block of (A . i) ; ::_thesis: x in S
 x c= product (Carrier A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in product (Carrier A) )
assume  a in x ; ::_thesis: a in product (Carrier A)
then consider g being Function such that
A4: g = a and
A5: dom g = dom B and
A6: for y being set st y in dom B holds
g . y in B . y by A2, CARD_3:def_5;
A7: for y being set st y in dom (Carrier A) holds
g . y in (Carrier A) . y
proof
let y be set ; ::_thesis: ( y in dom (Carrier A) implies g . y in (Carrier A) . y )
assume  y in dom (Carrier A) ; ::_thesis: g . y in (Carrier A) . y
then A8: y in I by PARTFUN1:def_2;
then  y in dom g by A5, PARTFUN1:def_2;
then A9: g . y in B . y by A5, A6;
 B c= Carrier A by PBOOLE:def_18;
then  B . y c= (Carrier A) . y by A8, PBOOLE:def_2;
hence  g . y in (Carrier A) . y by A9; ::_thesis: verum
end;
dom g = I by A5, PARTFUN1:def_2
.= dom (Carrier A) by PARTFUN1:def_2 ;
hence  a in product (Carrier A) by A4, A7, CARD_3:def_5; ::_thesis: verum
end;
hence  x in S by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of (product (Carrier A)) st ( for x being set holds
( x in b1 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) & ( for x being set holds
( x in b2 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) holds
b1 = b2
proof
let S1, S2 be Subset-Family of (product (Carrier A)); ::_thesis: ( ( for x being set holds
( x in S1 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) & ( for x being set holds
( x in S2 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) implies S1 = S2 )
assume that
A10: for x being set holds
( x in S1 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) and
A11: for x being set holds
( x in S2 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ; ::_thesis: S1 = S2
 for x being set holds
( x in S1 iff x in S2 )
proof
let x be set ; ::_thesis: ( x in S1 iff x in S2 )
 ( x in S1 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) by A10;
hence  ( x in S1 iff x in S2 ) by A11; ::_thesis: verum
end;
hence  S1 = S2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def_22_:_
 for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I
for b3 being Subset-Family of (product (Carrier A)) holds
( b3 = Segre_Blocks A iff for x being set holds
( x in b3 iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) );

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

:: deftheorem  defines Segre_Product PENCIL_1:def_23_:_
 for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I holds Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);

theorem Th14: :: PENCIL_1:14
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I
for x being Point of (Segre_Product A) holds x is ManySortedSet of I
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I
for x being Point of (Segre_Product A) holds x is ManySortedSet of I
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for x being Point of (Segre_Product A) holds x is ManySortedSet of I
let x be Point of (Segre_Product A); ::_thesis: x is ManySortedSet of I
 ex f being Function st
( x = f & dom f = dom (Carrier A) & ( for a being set st a in dom (Carrier A) holds
f . a in (Carrier A) . a ) ) by CARD_3:def_5;
hence  x is ManySortedSet of I ; ::_thesis: verum
end;

theorem Th15: :: PENCIL_1:15
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds
not Segre_Product A is void
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds
not Segre_Product A is void
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( not for i being Element of I holds A . i is void implies not Segre_Product A is void )
set B = the V2() trivial-yielding ManySortedSubset of Carrier A;
given i being Element of I such that A1: not A . i is void ; ::_thesis: not Segre_Product A is void
set l = the Block of (A . i);
A2: not the topology of (A . i) is empty by A1;
A3: the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) c= Carrier A
proof
let i1 be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i1 in I or ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 )
assume A4: i1 in I ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then A5: i1 in dom the V2() trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def_2;
percases ( i = i1 or i1 <> i ) ;
supposeA6: i = i1 ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then  ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 = the Block of (A . i) by A5, FUNCT_7:31;
then A7: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 in the topology of (A . i) by A2;
 ex R being 1-sorted st
( R = A . i1 & the carrier of R = (Carrier A) . i1 ) by A4, PRALG_1:def_13;
hence  ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 by A6, A7; ::_thesis: verum
end;
supposeA8: i1 <> i ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
A9: the V2() trivial-yielding ManySortedSubset of Carrier A c= Carrier A by PBOOLE:def_18;
 ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 = the V2() trivial-yielding ManySortedSubset of Carrier A . i1 by A8, FUNCT_7:32;
hence  ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 by A4, A9, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
 for j being Element of I st i <> j holds
( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element
proof
let j be Element of I; ::_thesis: ( i <> j implies ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element )
assume  i <> j ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element
then A10: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j = the V2() trivial-yielding ManySortedSubset of Carrier A . j by FUNCT_7:32;
 j in I ;
then A11: j in dom the V2() trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def_2;
then  ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j in rng the V2() trivial-yielding ManySortedSubset of Carrier A by A10, FUNCT_1:def_3;
then  ( not ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial ) by A11, A10, Def16, FUNCT_1:def_9;
hence  ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element ; ::_thesis: verum
end;
then reconsider C = the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) as Segre-like ManySortedSubset of Carrier A by A3, Def20, PBOOLE:def_18;
 dom the V2() trivial-yielding ManySortedSubset of Carrier A = I by PARTFUN1:def_2;
then  C . i is Block of (A . i) by FUNCT_7:31;
then  product C in Segre_Blocks A by Def22;
hence  not Segre_Product A is void by Def4; ::_thesis: verum
end;

theorem Th16: :: PENCIL_1:16
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds
not Segre_Product A is degenerated
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds
not Segre_Product A is degenerated
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) implies not Segre_Product A is degenerated )
assume A1: for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ; ::_thesis: not Segre_Product A is degenerated
then  not Segre_Product A is void by Th15;
then reconsider SB = Segre_Blocks A as non empty set ;
now__::_thesis:_not_product_(Carrier_A)_in_SB
assume  product (Carrier A) in SB ; ::_thesis: contradiction
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: product (Carrier A) = product B and
A3: ex i being Element of I st B . i is Block of (A . i) by Def22;
consider i being Element of I such that
A4: B . i is Block of (A . i) by A3;
 B is V2() by A2, Th1;
then  ( ex R being 1-sorted st
( R = A . i & the carrier of R = (Carrier A) . i ) & (Carrier A) . i is Block of (A . i) ) by A2, A4, PRALG_1:def_13, PUA2MSS1:2;
then  A . i is degenerated by Def5;
hence  contradiction by A1; ::_thesis: verum
end;
then  product (Carrier A) is not Element of SB ;
hence  not Segre_Product A is degenerated by Def5; ::_thesis: verum
end;

theorem Th17: :: PENCIL_1:17
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is with_non_trivial_blocks
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is with_non_trivial_blocks
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) implies Segre_Product A is with_non_trivial_blocks )
assume A1: for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ; ::_thesis: Segre_Product A is with_non_trivial_blocks
 for k being Block of (Segre_Product A) holds 2 c= card k
proof
let k be Block of (Segre_Product A); ::_thesis: 2 c= card k
 not Segre_Product A is void by A1, Th15;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: k = product B and
A3: ex i being Element of I st B . i is Block of (A . i) by Def22;
consider i being Element of I such that
A4: B . i is Block of (A . i) by A3;
 A . i is with_non_trivial_blocks by A1;
then  2 c= card (B . i) by A4, Def6;
then A5: not B . i is trivial by Th4;
 dom B = I by PARTFUN1:def_2;
then  B . i in rng B by FUNCT_1:def_3;
then reconsider BB = B as non trivial-yielding Segre-like ManySortedSet of I by A5, Def16;
 not product BB is trivial ;
hence  2 c= card k by A2, Th4; ::_thesis: verum
end;
hence  Segre_Product A is with_non_trivial_blocks by Def6; ::_thesis: verum
end;

theorem Th18: :: PENCIL_1:18
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is identifying_close_blocks
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is identifying_close_blocks
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) implies Segre_Product A is identifying_close_blocks )
assume A1: for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ; ::_thesis: Segre_Product A is identifying_close_blocks
 for k, l being Block of (Segre_Product A) st 2 c= card (k /\ l) holds
k = l
proof
let k, l be Block of (Segre_Product A); ::_thesis: ( 2 c= card (k /\ l) implies k = l )
assume  2 c= card (k /\ l) ; ::_thesis: k = l
then consider a, b being set  such that
A2: a in k /\ l and
A3: b in k /\ l and
A4: a <> b by Th2;
 not Segre_Product A is void by A1, Th15;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A5: k = product B and
A6: ex i being Element of I st B . i is Block of (A . i) by Def22;
A7: b in product B by A5, A3, XBOOLE_0:def_4;
then reconsider b = b as Function by CARD_3:48;
A8: dom b = dom B by A7, CARD_3:9
.= I by PARTFUN1:def_2 ;
then reconsider b = b as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A9: a in product B by A5, A2, XBOOLE_0:def_4;
consider i being Element of I such that
A10: B . i is Block of (A . i) by A6;
A11: for j being Element of I st j <> i holds
B . j is 1 -element
proof
let j be Element of I; ::_thesis: ( j <> i implies B . j is 1 -element )
assume A12: j <> i ; ::_thesis: B . j is 1 -element
consider i1 being Element of I such that
A13: for j1 being Element of I st j1 <> i1 holds
B . j1 is 1 -element by Def20;
 A . i is with_non_trivial_blocks by A1;
then  2 c= card (B . i) by A10, Def6;
then  not B . i is 1 -element by Th4;
then  i1 = i by A13;
hence  B . j is 1 -element by A12, A13; ::_thesis: verum
end;
 not Segre_Product A is void by A1, Th15;
then consider C being Segre-like ManySortedSubset of Carrier A such that
A14: l = product C and
A15: ex i being Element of I st C . i is Block of (A . i) by Def22;
A16: dom C = I by PARTFUN1:def_2;
consider j being Element of I such that
A17: C . j is Block of (A . j) by A15;
reconsider a = a as Function by A9, CARD_3:48;
A18: dom a = dom B by A9, CARD_3:9
.= I by PARTFUN1:def_2 ;
then reconsider a = a as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
consider x being set  such that
A19: x in I and
A20: a . x <> b . x by A4, A18, A8, FUNCT_1:2;
reconsider x = x as Element of I by A19;
 dom B = I by PARTFUN1:def_2;
then A21: b . x in B . x by A7, CARD_3:9;
 dom B = I by PARTFUN1:def_2;
then A22: a . x in B . x by A9, CARD_3:9;
then  2 c= card (B . x) by A20, A21, Th2;
then  not B . x is 1 -element by Th4;
then A23: x = i by A11;
 b in product C by A14, A3, XBOOLE_0:def_4;
then A24: b . x in C . x by A16, CARD_3:9;
A25: a in product C by A14, A2, XBOOLE_0:def_4;
A26: for i being Element of I st j <> i holds
C . i is 1 -element
proof
let i be Element of I; ::_thesis: ( j <> i implies C . i is 1 -element )
assume A27: j <> i ; ::_thesis: C . i is 1 -element
consider j1 being Element of I such that
A28: for i1 being Element of I st j1 <> i1 holds
C . i1 is 1 -element by Def20;
 A . j is with_non_trivial_blocks by A1;
then  2 c= card (C . j) by A17, Def6;
then  not C . j is 1 -element by Th4;
then  j1 = j by A28;
hence  C . i is 1 -element by A27, A28; ::_thesis: verum
end;
A29: dom B = I by PARTFUN1:def_2
.= dom C by PARTFUN1:def_2 ;
 dom C = I by PARTFUN1:def_2;
then A30: a . x in C . x by A25, CARD_3:9;
then  2 c= card (C . x) by A20, A24, Th2;
then  not C . x is 1 -element by Th4;
then A31: x = j by A26;
 for s being set st s in dom B holds
B . s c= C . s
proof
let s be set ; ::_thesis: ( s in dom B implies B . s c= C . s )
assume A32: s in dom B ; ::_thesis: B . s c= C . s
then reconsider t = s as Element of I by PARTFUN1:def_2;
percases ( t = x or s <> x ) ;
supposeA33: t = x ; ::_thesis: B . s c= C . s
then reconsider Ct = C . t as Block of (A . t) by A17, A31;
reconsider Bt = B . t as Block of (A . t) by A10, A23, A33;
 ( a . t in Bt /\ Ct & b . t in Bt /\ Ct ) by A22, A21, A30, A24, A33, XBOOLE_0:def_4;
then A34: 2 c= card (Bt /\ Ct) by A20, A33, Th2;
 A . t is identifying_close_blocks by A1;
hence  B . s c= C . s by A34, Def7; ::_thesis: verum
end;
suppose s <> x ; ::_thesis: B . s c= C . s
then  B . t is 1 -element by A11, A23;
then consider y being set  such that
A35: B . t = {y} by ZFMISC_1:131;
A36: a . t in C . t by A25, A29, A32, CARD_3:9;
 a . t in B . t by A9, A32, CARD_3:9;
then  a . t = y by A35, TARSKI:def_1;
hence  B . s c= C . s by A35, A36, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence  k c= l by A5, A14, A29, CARD_3:27; :: according to XBOOLE_0:def_10 ::_thesis: l c= k
 for s being set st s in dom C holds
C . s c= B . s
proof
let s be set ; ::_thesis: ( s in dom C implies C . s c= B . s )
assume A37: s in dom C ; ::_thesis: C . s c= B . s
then reconsider t = s as Element of I by PARTFUN1:def_2;
percases ( t = x or s <> x ) ;
supposeA38: t = x ; ::_thesis: C . s c= B . s
then reconsider Ct = C . t as Block of (A . t) by A17, A31;
reconsider Bt = B . t as Block of (A . t) by A10, A23, A38;
 ( a . t in Bt /\ Ct & b . t in Bt /\ Ct ) by A22, A21, A30, A24, A38, XBOOLE_0:def_4;
then A39: 2 c= card (Bt /\ Ct) by A20, A38, Th2;
 A . t is identifying_close_blocks by A1;
hence  C . s c= B . s by A39, Def7; ::_thesis: verum
end;
suppose s <> x ; ::_thesis: C . s c= B . s
then  C . t is 1 -element by A26, A31;
then consider y being set  such that
A40: C . t = {y} by ZFMISC_1:131;
A41: a . t in B . t by A9, A29, A37, CARD_3:9;
 a . t in C . t by A25, A37, CARD_3:9;
then  a . t = y by A40, TARSKI:def_1;
hence  C . s c= B . s by A40, A41, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence  l c= k by A5, A14, A29, CARD_3:27; ::_thesis: verum
end;
hence  Segre_Product A is identifying_close_blocks by Def7; ::_thesis: verum
end;

registration
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
cluster Segre_Product A ->  non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ;
coherence
 ( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks )
proof
A1: ( ( for j being Element of I holds A . j is with_non_trivial_blocks ) & ( for j being Element of I holds A . j is identifying_close_blocks ) ) ;
 ( not A . the Element of I is void & ( for j being Element of I holds not A . j is degenerated ) ) ;
hence  ( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks ) by A1, Th15, Th16, Th17, Th18; ::_thesis: verum
end;
end;

theorem :: PENCIL_1:19
for T being TopStruct
for S being Subset of T st S is trivial holds
( S is strong & S is closed_under_lines )
proof
let T be TopStruct ; ::_thesis: for S being Subset of T st S is trivial holds
( S is strong & S is closed_under_lines )
let S be Subset of T; ::_thesis: ( S is trivial implies ( S is strong & S is closed_under_lines ) )
assume A1: S is trivial ; ::_thesis: ( S is strong & S is closed_under_lines )
thus  S is strong ::_thesis: S is closed_under_lines
proof
let x, y be Point of T; :: according to PENCIL_1:def_3 ::_thesis: ( x in S & y in S implies x,y are_collinear )
assume A2: ( x in S & y in S ) ; ::_thesis: x,y are_collinear
thus  x,y are_collinear ::_thesis: verum
proof
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: x,y are_collinear
hence  x,y are_collinear by Def1; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: x,y are_collinear
then  2 c= card S by A2, Th2;
hence  x,y are_collinear by A1, Th4; ::_thesis: verum
end;
end;
end;
end;
thus  S is closed_under_lines ::_thesis: verum
proof
let l be Block of T; :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (l /\ S) implies l c= S )
A3: card (l /\ S) c= card S by CARD_1:11, XBOOLE_1:17;
assume  2 c= card (l /\ S) ; ::_thesis: l c= S
then  2 c= card S by A3, XBOOLE_1:1;
hence  l c= S by A1, Th4; ::_thesis: verum
end;
end;

theorem Th20: :: PENCIL_1:20
for S being identifying_close_blocks TopStruct
for l being Block of S
for L being Subset of S st L = l holds
L is closed_under_lines
proof
let S be identifying_close_blocks TopStruct ; ::_thesis: for l being Block of S
for L being Subset of S st L = l holds
L is closed_under_lines
let l be Block of S; ::_thesis: for L being Subset of S st L = l holds
L is closed_under_lines
let L be Subset of S; ::_thesis: ( L = l implies L is closed_under_lines )
assume A1: L = l ; ::_thesis: L is closed_under_lines
thus  L is closed_under_lines ::_thesis: verum
proof
let K be Block of S; :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (K /\ L) implies K c= L )
assume  2 c= card (K /\ L) ; ::_thesis: K c= L
hence  K c= L by A1, Def7; ::_thesis: verum
end;
end;

theorem Th21: :: PENCIL_1:21
for S being TopStruct
for l being Block of S
for L being Subset of S st L = l holds
L is strong
proof
let S be TopStruct ; ::_thesis: for l being Block of S
for L being Subset of S st L = l holds
L is strong
let l be Block of S; ::_thesis: for L being Subset of S st L = l holds
L is strong
let L be Subset of S; ::_thesis: ( L = l implies L is strong )
assume A1: L = l ; ::_thesis: L is strong
thus  L is strong ::_thesis: verum
proof
let x, y be Point of S; :: according to PENCIL_1:def_3 ::_thesis: ( x in L & y in L implies x,y are_collinear )
assume  ( x in L & y in L ) ; ::_thesis: x,y are_collinear
then  {x,y} c= l by A1, ZFMISC_1:32;
hence  x,y are_collinear by Def1; ::_thesis: verum
end;
end;

theorem :: PENCIL_1:22
for S being non void TopStruct holds [#] S is closed_under_lines
proof
let S be non void TopStruct ; ::_thesis: [#] S is closed_under_lines
thus  [#] S is closed_under_lines ::_thesis: verum
proof
let K be Block of S; :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (K /\ ([#] S)) implies K c= [#] S )
assume  2 c= card (K /\ ([#] S)) ; ::_thesis: K c= [#] S
 K in the topology of S ;
hence  K c= [#] S ; ::_thesis: verum
end;
end;

theorem Th23: :: PENCIL_1:23
for I being non empty set
for A being non trivial-yielding Segre-like ManySortedSet of I
for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being set st i <> indx A holds
x . i = y . i
proof
let I be non empty set ; ::_thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being set st i <> indx A holds
x . i = y . i
let A be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being set st i <> indx A holds
x . i = y . i
let x, y be ManySortedSet of I; ::_thesis: ( x in product A & y in product A implies for i being set st i <> indx A holds
x . i = y . i )
assume that
A1: x in product A and
A2: y in product A ; ::_thesis: for i being set st i <> indx A holds
x . i = y . i
let i be set ; ::_thesis: ( i <> indx A implies x . i = y . i )
A3: dom A = I by PARTFUN1:def_2;
assume A4: i <> indx A ; ::_thesis: x . i = y . i
percases ( not i in I or i in I ) ;
supposeA5: not i in I ; ::_thesis: x . i = y . i
then A6: not i in dom y by PARTFUN1:def_2;
 not i in dom x by A5, PARTFUN1:def_2;
hence x . i = {} by FUNCT_1:def_2
.= y . i by A6, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose i in I ; ::_thesis: x . i = y . i
then reconsider ii = i as Element of I ;
consider j being Element of I such that
A7: for k being Element of I st k <> j holds
A . k is 1 -element by Def20;
now__::_thesis:_not_j_<>_indx_A
assume  j <> indx A ; ::_thesis: contradiction
then  A . (indx A) is 1 -element by A7;
hence  contradiction by Def21; ::_thesis: verum
end;
then  A . ii is 1 -element by A4, A7;
then consider o being set  such that
A8: A . i = {o} by ZFMISC_1:131;
A9: x . ii in A . ii by A1, A3, CARD_3:9;
 y . ii in A . ii by A2, A3, CARD_3:9;
hence y . i = o by A8, TARSKI:def_1
.= x . i by A8, A9, TARSKI:def_1 ;
::_thesis: verum
end;
end;
end;

theorem Th24: :: PENCIL_1:24
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
let x be set ; ::_thesis: ( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
thus  ( x is Block of (Segre_Product A) implies ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) ) ::_thesis: ( ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) implies x is Block of (Segre_Product A) )
proof
assume A1: x is Block of (Segre_Product A) ; ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) )
then consider L being Segre-like ManySortedSubset of Carrier A such that
A2: x = product L and
A3: ex i being Element of I st L . i is Block of (A . i) by Def22;
 2 c= card (product L) by A1, A2, Def6;
then reconsider L = L as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th13;
consider i being Element of I such that
A4: L . i is Block of (A . i) by A3;
now__::_thesis:_not_i_<>_indx_L
assume  i <> indx L ; ::_thesis: contradiction
then A5: L . i is 1 -element by Th12;
 2 c= card (L . i) by A4, Def6;
hence  contradiction by A5, Th4; ::_thesis: verum
end;
hence  ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) by A2, A4; ::_thesis: verum
end;
given L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: ( x = product L & L . (indx L) is Block of (A . (indx L)) ) ; ::_thesis: x is Block of (Segre_Product A)
thus  x is Block of (Segre_Product A) by A6, Def22; ::_thesis: verum
end;

theorem Th25: :: PENCIL_1:25
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for P being ManySortedSet of I st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for P being ManySortedSet of I st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
let A be PLS-yielding ManySortedSet of I; ::_thesis: for P being ManySortedSet of I st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
let P be ManySortedSet of I; ::_thesis: ( P is Point of (Segre_Product A) implies for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A) )
assume A1: P is Point of (Segre_Product A) ; ::_thesis: for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
let j be Element of I; ::_thesis: for p being Point of (A . j) holds P +* (j,p) is Point of (Segre_Product A)
let p be Point of (A . j); ::_thesis: P +* (j,p) is Point of (Segre_Product A)
A2: for i being set st i in dom (Carrier A) holds
(P +* (j,p)) . i in (Carrier A) . i
proof
let i be set ; ::_thesis: ( i in dom (Carrier A) implies (P +* (j,p)) . i in (Carrier A) . i )
assume A3: i in dom (Carrier A) ; ::_thesis: (P +* (j,p)) . i in (Carrier A) . i
then  i in I by PARTFUN1:def_2;
then A4: i in dom P by PARTFUN1:def_2;
percases ( i <> j or i = j ) ;
suppose i <> j ; ::_thesis: (P +* (j,p)) . i in (Carrier A) . i
then  (P +* (j,p)) . i = P . i by FUNCT_7:32;
hence  (P +* (j,p)) . i in (Carrier A) . i by A1, A3, CARD_3:9; ::_thesis: verum
end;
supposeA5: i = j ; ::_thesis: (P +* (j,p)) . i in (Carrier A) . i
A6: p in the carrier of (A . j) ;
 (P +* (j,p)) . i = p by A4, A5, FUNCT_7:31;
hence  (P +* (j,p)) . i in (Carrier A) . i by A5, A6, YELLOW_6:2; ::_thesis: verum
end;
end;
end;
dom (P +* (j,p)) = I by PARTFUN1:def_2
.= dom (Carrier A) by PARTFUN1:def_2 ;
hence  P +* (j,p) is Point of (Segre_Product A) by A2, CARD_3:9; ::_thesis: verum
end;

theorem Th26: :: PENCIL_1:26
for I being non empty set
for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds
( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
proof
let I be non empty set ; ::_thesis: for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds
( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
let A, B be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: ( 2 c= card ((product A) /\ (product B)) implies ( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) ) )
A1: dom B = I by PARTFUN1:def_2;
assume  2 c= card ((product A) /\ (product B)) ; ::_thesis: ( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
then consider a, b being set  such that
A2: a in (product A) /\ (product B) and
A3: b in (product A) /\ (product B) and
A4: a <> b by Th2;
 b in product A by A3, XBOOLE_0:def_4;
then consider b1 being Function such that
A5: b1 = b and
A6: dom b1 = dom A and
A7: for o being set st o in dom A holds
b1 . o in A . o by CARD_3:def_5;
 a in product A by A2, XBOOLE_0:def_4;
then consider a1 being Function such that
A8: a1 = a and
A9: dom a1 = dom A and
A10: for o being set st o in dom A holds
a1 . o in A . o by CARD_3:def_5;
consider o being set  such that
A11: o in dom A and
A12: a1 . o <> b1 . o by A4, A8, A9, A5, A6, FUNCT_1:2;
reconsider o = o as Element of I by A11, PARTFUN1:def_2;
 b in product B by A3, XBOOLE_0:def_4;
then A13: b1 . o in B . o by A5, A1, CARD_3:9;
A14: a in product B by A2, XBOOLE_0:def_4;
then  a1 . o in B . o by A8, A1, CARD_3:9;
then  2 c= card (B . o) by A12, A13, Th2;
then A15: not B . o is trivial by Th4;
then A16: o = indx B by Def21;
A17: b1 . o in A . o by A7, A11;
 a1 . o in A . o by A10, A11;
then  2 c= card (A . o) by A12, A17, Th2;
then  not A . o is trivial by Th4;
then A18: o = indx A by Def21;
hence  indx A = indx B by A15, Def21; ::_thesis: for i being set st i <> indx A holds
A . i = B . i
let i be set ; ::_thesis: ( i <> indx A implies A . i = B . i )
assume A19: i <> indx A ; ::_thesis: A . i = B . i
percases ( i in I or not i in I ) ;
supposeA20: i in I ; ::_thesis: A . i = B . i
then  B . i is 1 -element by A18, A16, A19, Th12;
then A21: ex y being set st B . i = {y} by ZFMISC_1:131;
 A . i is 1 -element by A19, A20, Th12;
then consider x being set  such that
A22: A . i = {x} by ZFMISC_1:131;
 dom B = I by PARTFUN1:def_2;
then A23: a1 . i in B . i by A8, A14, A20, CARD_3:9;
 dom A = I by PARTFUN1:def_2;
then  a1 . i in A . i by A10, A20;
then  a1 . i = x by A22, TARSKI:def_1;
hence  A . i = B . i by A22, A21, A23, TARSKI:def_1; ::_thesis: verum
end;
supposeA24: not i in I ; ::_thesis: A . i = B . i
then A25: not i in dom B by PARTFUN1:def_2;
 not i in dom A by A24, PARTFUN1:def_2;
hence A . i = {} by FUNCT_1:def_2
.= B . i by A25, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;

theorem Th27: :: PENCIL_1:27
for I being non empty set
for A being non trivial-yielding Segre-like ManySortedSet of I
for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
proof
let I be non empty set ; ::_thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
let A be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
let N be non trivial set ; ::_thesis: ( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
thus  A +* ((indx A),N) is Segre-like ::_thesis: not A +* ((indx A),N) is trivial-yielding
proof
take  indx A ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st indx A <> j holds
(A +* ((indx A),N)) . j is 1 -element
let i be Element of I; ::_thesis: ( indx A <> i implies (A +* ((indx A),N)) . i is 1 -element )
assume A1: i <> indx A ; ::_thesis: (A +* ((indx A),N)) . i is 1 -element
then  (A +* ((indx A),N)) . i = A . i by FUNCT_7:32;
hence  (A +* ((indx A),N)) . i is 1 -element by A1, Th12; ::_thesis: verum
end;
thus  not A +* ((indx A),N) is trivial-yielding ::_thesis: verum
proof
take  (A +* ((indx A),N)) . (indx A) ; :: according to PENCIL_1:def_16 ::_thesis: ( (A +* ((indx A),N)) . (indx A) in rng (A +* ((indx A),N)) & not (A +* ((indx A),N)) . (indx A) is trivial )
 dom (A +* ((indx A),N)) = I by PARTFUN1:def_2;
hence  (A +* ((indx A),N)) . (indx A) in rng (A +* ((indx A),N)) by FUNCT_1:def_3; ::_thesis: not (A +* ((indx A),N)) . (indx A) is trivial
 I = dom A by PARTFUN1:def_2;
hence  not (A +* ((indx A),N)) . (indx A) is trivial by FUNCT_7:31; ::_thesis: verum
end;
end;

theorem :: PENCIL_1:28
for S being non empty non void identifying_close_blocks without_isolated_points TopStruct st S is strongly_connected holds
S is connected
proof
let S be non empty non void identifying_close_blocks without_isolated_points TopStruct ; ::_thesis: ( S is strongly_connected implies S is connected )
assume A1: S is strongly_connected ; ::_thesis: S is connected
thus  S is connected ::_thesis: verum
proof
let x, y be Point of S; :: according to PENCIL_1:def_10 ::_thesis: ex f being FinSequence of the carrier of S st
( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) )
A2: len <*x*> = 1 by FINSEQ_1:39;
A3: len <*y*> = 1 by FINSEQ_1:39;
consider K being Block of S such that
A4: x in K by Def9;
 K in the topology of S ;
then reconsider L = K as Subset of S ;
 ( L is closed_under_lines & L is strong ) by Th20, Th21;
then consider f being FinSequence of bool the carrier of S such that
A5: L = f . 1 and
A6: y in f . (len f) and
A7: for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) and
A8: for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by A1, Def11;
A9: len f in dom f by A6, FUNCT_1:def_2;
A10: 1 in dom f by A4, A5, FUNCT_1:def_2;
then reconsider n = (len f) - 1 as Nat by FINSEQ_3:26;
deffunc H1( Nat) ->  set = (f . $1) /\ (f . ($1 + 1));
reconsider n = n as Element of NAT by ORDINAL1:def_12;
consider h being FinSequence such that
A11: ( len h = n & ( for k being Nat st k in dom h holds
h . k = H1(k) ) ) from FINSEQ_1:sch_2();
A12: dom h = Seg n by A11, FINSEQ_1:def_3;
A13: (len h) + 1 = len f by A11;
now__::_thesis:_not_{}_in_rng_h
assume  {} in rng h ; ::_thesis: contradiction
then consider i being set  such that
A14: i in dom h and
A15: h . i = {} by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A14;
A16: i <= len h by A14, FINSEQ_3:25;
then A17: i < len f by A13, NAT_1:13;
A18: 1 <= i by A14, FINSEQ_3:25;
then  i in Seg n by A11, A16, FINSEQ_1:1;
then  h . i = (f . i) /\ (f . (i + 1)) by A11, A12;
then  2 c= card (h . i) by A8, A18, A17;
hence  contradiction by A15; ::_thesis: verum
end;
then  product h <> {} by CARD_3:26;
then consider c being set  such that
A19: c in product h by XBOOLE_0:def_1;
A20: ex ce being Function st
( ce = c & dom ce = dom h & ( for a being set st a in dom h holds
ce . a in h . a ) ) by A19, CARD_3:def_5;
then reconsider c = c as Function ;
A21: dom h = Seg n by A11, FINSEQ_1:def_3;
then reconsider c = c as FinSequence by A20, FINSEQ_1:def_2;
A22: rng f c= bool the carrier of S by FINSEQ_1:def_4;
 rng ((<*x*> ^ c) ^ <*y*>) c= the carrier of S
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng ((<*x*> ^ c) ^ <*y*>) or r in the carrier of S )
assume  r in rng ((<*x*> ^ c) ^ <*y*>) ; ::_thesis: r in the carrier of S
then  r in (rng (<*x*> ^ c)) \/ (rng <*y*>) by FINSEQ_1:31;
then  ( r in rng (<*x*> ^ c) or r in rng <*y*> ) by XBOOLE_0:def_3;
then A23: ( r in (rng <*x*>) \/ (rng c) or r in rng <*y*> ) by FINSEQ_1:31;
percases ( r in rng <*x*> or r in rng c or r in rng <*y*> ) by A23, XBOOLE_0:def_3;
suppose r in rng <*x*> ; ::_thesis: r in the carrier of S
then  r in {x} by FINSEQ_1:38;
hence  r in the carrier of S ; ::_thesis: verum
end;
suppose r in rng c ; ::_thesis: r in the carrier of S
then consider o being set  such that
A24: o in dom c and
A25: r = c . o by FUNCT_1:def_3;
reconsider o = o as Element of NAT by A24;
 h . o = (f . o) /\ (f . (o + 1)) by A11, A20, A24;
then  r in (f . o) /\ (f . (o + 1)) by A20, A24, A25;
then A26: r in f . o by XBOOLE_0:def_4;
 len h <= len f by A13, NAT_1:11;
then  dom h c= dom f by FINSEQ_3:30;
then  f . o in rng f by A20, A24, FUNCT_1:def_3;
hence  r in the carrier of S by A22, A26; ::_thesis: verum
end;
suppose r in rng <*y*> ; ::_thesis: r in the carrier of S
then  r in {y} by FINSEQ_1:38;
hence  r in the carrier of S ; ::_thesis: verum
end;
end;
end;
then reconsider g = (<*x*> ^ c) ^ <*y*> as FinSequence of the carrier of S by FINSEQ_1:def_4;
A27: len (<*x*> ^ c) = (len <*x*>) + (len c) by FINSEQ_1:22;
then A28: len (<*x*> ^ c) = (len c) + 1 by FINSEQ_1:39;
take  g ; ::_thesis: ( x = g . 1 & y = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear ) )
A29: g = <*x*> ^ (c ^ <*y*>) by FINSEQ_1:32;
hence  x = g . 1 by FINSEQ_1:41; ::_thesis: ( y = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear ) )
 len g = (len (<*x*> ^ c)) + (len <*y*>) by FINSEQ_1:22;
then A30: (len (<*x*> ^ c)) + 1 = len g by FINSEQ_1:39;
hence A31: y = g . (len g) by FINSEQ_1:42; ::_thesis: for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear
let i be Nat; ::_thesis: ( 1 <= i & i < len g implies for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear )
assume that
A32: 1 <= i and
A33: i < len g ; ::_thesis: for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear
A34: i <= len (<*x*> ^ c) by A30, A33, NAT_1:13;
let a, b be Point of S; ::_thesis: ( a = g . i & b = g . (i + 1) implies a,b are_collinear )
assume that
A35: a = g . i and
A36: b = g . (i + 1) ; ::_thesis: a,b are_collinear
reconsider i = i as Element of NAT by ORDINAL1:def_12;
percases ( ( i = 1 & i <= len c ) or ( i = 1 & i = (len c) + 1 ) or ( 1 < i & i <= len c ) or ( 1 < i & i = (len c) + 1 ) ) by A28, A32, A34, NAT_1:8, XXREAL_0:1;
supposeA37: ( i = 1 & i <= len c ) ; ::_thesis: a,b are_collinear
 ( len (c ^ <*y*>) = (len c) + 1 & len (<*x*> ^ (c ^ <*y*>)) = (len <*x*>) + (len (c ^ <*y*>)) ) by A3, FINSEQ_1:22;
then A38: len (<*x*> ^ (c ^ <*y*>)) = (1 + 1) + (len c) by A2;
A39: 1 in dom c by A37, FINSEQ_3:25;
 b = (<*x*> ^ (c ^ <*y*>)) . 2 by A36, A37, FINSEQ_1:32;
then  b = (c ^ <*y*>) . (2 - (len <*x*>)) by A2, A38, FINSEQ_1:24, NAT_1:11;
then  b = (c ^ <*y*>) . (2 - 1) by FINSEQ_1:39;
then A40: b = c . 1 by A39, FINSEQ_1:def_7;
 ( c . 1 in h . 1 & h . 1 = (f . 1) /\ (f . (1 + 1)) ) by A11, A20, A39;
then A41: b in f . 1 by A40, XBOOLE_0:def_4;
A42: f . 1 in rng f by A10, FUNCT_1:def_3;
then reconsider f1 = f . 1 as Subset of S by A22;
A43: ( f1 is closed_under_lines & f1 is strong ) by A7, A42;
 a = x by A29, A35, A37, FINSEQ_1:41;
hence  a,b are_collinear by A4, A5, A41, A43, Def3; ::_thesis: verum
end;
supposeA44: ( i = 1 & i = (len c) + 1 ) ; ::_thesis: a,b are_collinear
A45: f . 1 in rng f by A10, FUNCT_1:def_3;
then reconsider f1 = f . 1 as Subset of S by A22;
A46: ( f1 is closed_under_lines & f1 is strong ) by A7, A45;
 len <*x*> = 1 by FINSEQ_1:39;
then A47: len g = i + 1 by A30, A44, FINSEQ_1:22;
 len h = 0 by A20, A44, FINSEQ_3:29;
then  x,y are_collinear by A4, A5, A6, A11, A46, Def3;
hence  a,b are_collinear by A29, A31, A35, A36, A44, A47, FINSEQ_1:41; ::_thesis: verum
end;
supposeA48: ( 1 < i & i <= len c ) ; ::_thesis: a,b are_collinear
A49: ( len h <= (len h) + 1 & len c = len h ) by A20, FINSEQ_3:29, NAT_1:11;
then  i <= (len h) + 1 by A48, XXREAL_0:2;
then A50: i in dom f by A11, A48, FINSEQ_3:25;
then reconsider j = i - 1 as Nat by FINSEQ_3:26;
 i <= (len c) + 1 by A48, A49, XXREAL_0:2;
then  i in dom (<*x*> ^ c) by A28, A48, FINSEQ_3:25;
then A51: a = (<*x*> ^ c) . i by A35, FINSEQ_1:def_7;
 i <= len (<*x*> ^ c) by A27, A2, A48, NAT_1:13;
then A52: a = c . j by A2, A48, A51, FINSEQ_1:24;
 j + 1 = i ;
then A53: 1 <= j by A48, NAT_1:13;
A54: f . i in rng f by A50, FUNCT_1:def_3;
then reconsider ff = f . i as Subset of S by A22;
A55: j <= j + 1 by NAT_1:11;
A56: ( len <*x*> < i + 1 & i + 1 <= (len c) + 1 ) by A2, A48, NAT_1:13, XREAL_1:6;
then  i + 1 in dom (<*x*> ^ c) by A27, A2, FINSEQ_3:25;
then  b = (<*x*> ^ c) . (i + 1) by A36, FINSEQ_1:def_7;
then A57: b = c . ((i + 1) - (len <*x*>)) by A28, A56, FINSEQ_1:24;
 i <= len h by A20, A48, FINSEQ_3:29;
then A58: i in Seg n by A11, A48, FINSEQ_1:1;
then  c . i in h . i by A20, A21;
then  b in (f . i) /\ (f . (i + 1)) by A11, A12, A2, A58, A57;
then A59: b in ff by XBOOLE_0:def_4;
 i <= len h by A20, A48, FINSEQ_3:29;
then  j <= n by A11, A55, XXREAL_0:2;
then A60: j in Seg n by A53, FINSEQ_1:1;
then  c . j in h . j by A20, A21;
then  a in (f . j) /\ (f . (j + 1)) by A11, A12, A60, A52;
then A61: a in ff by XBOOLE_0:def_4;
 ( ff is closed_under_lines & ff is strong ) by A7, A54;
hence  a,b are_collinear by A61, A59, Def3; ::_thesis: verum
end;
supposeA62: ( 1 < i & i = (len c) + 1 ) ; ::_thesis: a,b are_collinear
then  0 + 1 < (len c) + 1 ;
then  ex k being Nat st len c = k + 1 by NAT_1:6;
then  1 <= len c by NAT_1:11;
then A63: len c in dom h by A20, FINSEQ_3:25;
A64: len (<*x*> ^ c) = 1 + (len c) by A2, FINSEQ_1:22;
then  i in dom (<*x*> ^ c) by A62, FINSEQ_3:25;
then a = (<*x*> ^ c) . i by A35, FINSEQ_1:def_7
.= c . (((len c) + 1) - 1) by A2, A62, A64, FINSEQ_1:24
.= c . (len c) ;
then  a in h . (len c) by A20, A63;
then A65: a in (f . (len c)) /\ (f . ((len c) + 1)) by A11, A63;
A66: f . (len f) in rng f by A9, FUNCT_1:def_3;
then reconsider ff = f . (len f) as Subset of S by A22;
A67: ( ff is closed_under_lines & ff is strong ) by A7, A66;
 len c = len h by A20, FINSEQ_3:29;
then A68: a in ff by A11, A65, XBOOLE_0:def_4;
 b = y by A36, A62, A64, FINSEQ_1:42;
hence  a,b are_collinear by A6, A67, A68, Def3; ::_thesis: verum
end;
end;
end;
end;

theorem :: PENCIL_1:29
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
let S be Subset of (Segre_Product A); ::_thesis: ( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) )
thus  ( not S is trivial & S is strong & S is closed_under_lines implies ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) ) ::_thesis: ( ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) implies ( not S is trivial & S is strong & S is closed_under_lines ) )
proof
assume A1: ( not S is trivial & S is strong & S is closed_under_lines ) ; ::_thesis: ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) )
then  2 c= card S by Th4;
then consider a, b being set  such that
A2: a in S and
A3: b in S and
A4: a <> b by Th2;
reconsider a = a, b = b as Point of (Segre_Product A) by A2, A3;
 a,b are_collinear by A1, A2, A3, Def3;
then consider C being Block of (Segre_Product A) such that
A5: {a,b} c= C by A4, Def1;
consider CC being Segre-like ManySortedSubset of Carrier A such that
A6: C = product CC and
 ex i being Element of I st CC . i is Block of (A . i) by Def22;
 ( a in product CC & b in product CC ) by A5, A6, ZFMISC_1:32;
then  2 c= card (product CC) by A4, Th2;
then reconsider CC = CC as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th13;
A7: dom CC = I by PARTFUN1:def_2;
reconsider a1 = a, b1 = b as ManySortedSet of I by Th14;
A8: dom a1 = I by PARTFUN1:def_2;
A9: dom b1 = I by PARTFUN1:def_2;
A10: now__::_thesis:_not_a1_._(indx_CC)_=_b1_._(indx_CC)
assume A11: a1 . (indx CC) = b1 . (indx CC) ; ::_thesis: contradiction
 for i being set st i in I holds
a1 . i = b1 . i
proof
let i be set ; ::_thesis: ( i in I implies a1 . i = b1 . i )
assume  i in I ; ::_thesis: a1 . i = b1 . i
percases ( i = indx CC or i <> indx CC ) ;
suppose i = indx CC ; ::_thesis: a1 . i = b1 . i
hence  a1 . i = b1 . i by A11; ::_thesis: verum
end;
supposeA12: i <> indx CC ; ::_thesis: a1 . i = b1 . i
 ( a1 in product CC & b1 in product CC ) by A5, A6, ZFMISC_1:32;
hence  a1 . i = b1 . i by A12, Th23; ::_thesis: verum
end;
end;
end;
hence  contradiction by A4, A8, A9, FUNCT_1:2; ::_thesis: verum
end;
A13: for f being ManySortedSet of I st f in S holds
for i being Element of I st i <> indx CC holds
f . i in CC . i
proof
let f be ManySortedSet of I; ::_thesis: ( f in S implies for i being Element of I st i <> indx CC holds
f . i in CC . i )
assume A14: f in S ; ::_thesis: for i being Element of I st i <> indx CC holds
f . i in CC . i
then reconsider f1 = f as Point of (Segre_Product A) ;
let i be Element of I; ::_thesis: ( i <> indx CC implies f . i in CC . i )
assume A15: i <> indx CC ; ::_thesis: f . i in CC . i
now__::_thesis:_f_._i_in_CC_._i
 b1 in product CC by A5, A6, ZFMISC_1:32;
then A16: b1 . i in CC . i by A7, CARD_3:9;
assume A17: not f . i in CC . i ; ::_thesis: contradiction
 f1,b are_collinear by A1, A3, A14, Def3;
then consider lb being Block of (Segre_Product A) such that
A18: {f1,b} c= lb by A17, A16, Def1;
consider Lb being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A19: lb = product Lb and
 Lb . (indx Lb) is Block of (A . (indx Lb)) by Th24;
A20: b1 in product Lb by A18, A19, ZFMISC_1:32;
A21: f in product Lb by A18, A19, ZFMISC_1:32;
then  indx Lb = i by A17, A16, A20, Th23;
then  Lb . (indx CC) is 1 -element by A15, Th12;
then consider cb being set  such that
A22: Lb . (indx CC) = {cb} by ZFMISC_1:131;
A23: dom Lb = I by PARTFUN1:def_2;
then  b1 . (indx CC) in {cb} by A20, A22, CARD_3:9;
then A24: b1 . (indx CC) = cb by TARSKI:def_1;
 a1 in product CC by A5, A6, ZFMISC_1:32;
then A25: a1 . i in CC . i by A7, CARD_3:9;
 f1,a are_collinear by A1, A2, A14, Def3;
then consider la being Block of (Segre_Product A) such that
A26: {f1,a} c= la by A17, A25, Def1;
consider La being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A27: la = product La and
 La . (indx La) is Block of (A . (indx La)) by Th24;
A28: a1 in product La by A26, A27, ZFMISC_1:32;
A29: f in product La by A26, A27, ZFMISC_1:32;
then  indx La = i by A17, A25, A28, Th23;
then  La . (indx CC) is 1 -element by A15, Th12;
then consider ca being set  such that
A30: La . (indx CC) = {ca} by ZFMISC_1:131;
A31: dom La = I by PARTFUN1:def_2;
then  a1 . (indx CC) in {ca} by A28, A30, CARD_3:9;
then A32: ca <> cb by A10, A24, TARSKI:def_1;
 f . (indx CC) in {ca} by A29, A30, A31, CARD_3:9;
then A33: f . (indx CC) <> cb by A32, TARSKI:def_1;
 f . (indx CC) in {cb} by A21, A22, A23, CARD_3:9;
hence  contradiction by A33, TARSKI:def_1; ::_thesis: verum
end;
hence  f . i in CC . i ; ::_thesis: verum
end;
 ( a1 . (indx CC) in pi (S,(indx CC)) & b1 . (indx CC) in pi (S,(indx CC)) ) by A2, A3, CARD_3:def_6;
then  2 c= card (pi (S,(indx CC))) by A10, Th2;
then reconsider p = pi (S,(indx CC)) as non trivial set by Th4;
 CC +* ((indx CC),p) c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (CC +* ((indx CC),p)) . i c= (Carrier A) . i )
assume A34: i in I ; ::_thesis: (CC +* ((indx CC),p)) . i c= (Carrier A) . i
percases ( i <> indx CC or i = indx CC ) ;
supposeA35: i <> indx CC ; ::_thesis: (CC +* ((indx CC),p)) . i c= (Carrier A) . i
A36: CC c= Carrier A by PBOOLE:def_18;
 (CC +* ((indx CC),p)) . i = CC . i by A35, FUNCT_7:32;
hence  (CC +* ((indx CC),p)) . i c= (Carrier A) . i by A34, A36, PBOOLE:def_2; ::_thesis: verum
end;
supposeA37: i = indx CC ; ::_thesis: (CC +* ((indx CC),p)) . i c= (Carrier A) . i
A38: p c= (Carrier A) . i
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p or y in (Carrier A) . i )
assume  y in p ; ::_thesis: y in (Carrier A) . i
then A39: ex f being Function st
( f in S & y = f . i ) by A37, CARD_3:def_6;
 i in dom (Carrier A) by A34, PARTFUN1:def_2;
hence  y in (Carrier A) . i by A39, CARD_3:9; ::_thesis: verum
end;
 dom CC = I by PARTFUN1:def_2;
hence  (CC +* ((indx CC),p)) . i c= (Carrier A) . i by A37, A38, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
then reconsider B = CC +* ((indx CC),p) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th27, PBOOLE:def_18;
take  B ; ::_thesis: ( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) )
A40: dom B = I by PARTFUN1:def_2;
A41: B . (indx CC) = p by A7, FUNCT_7:31;
thus A42: S = product B ::_thesis: for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines )
proof
thus  S c= product B :: according to XBOOLE_0:def_10 ::_thesis: product B c= S
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in S or e in product B )
assume A43: e in S ; ::_thesis: e in product B
then reconsider f = e as ManySortedSet of I by Th14;
A44: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
f_._i_in_B_._i
let i be set ; ::_thesis: ( i in I implies f . b1 in B . b1 )
assume  i in I ; ::_thesis: f . b1 in B . b1
then reconsider j = i as Element of I ;
percases ( j = indx CC or j <> indx CC ) ;
suppose j = indx CC ; ::_thesis: f . b1 in B . b1
hence  f . i in B . i by A41, A43, CARD_3:def_6; ::_thesis: verum
end;
supposeA45: j <> indx CC ; ::_thesis: f . b1 in B . b1
then  f . j in CC . j by A13, A43;
hence  f . i in B . i by A45, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
 dom f = I by PARTFUN1:def_2;
hence  e in product B by A40, A44, CARD_3:9; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in product B or e in S )
assume  e in product B ; ::_thesis: e in S
then consider f being Function such that
A46: ( e = f & dom f = I ) and
A47: for i being set st i in I holds
f . i in B . i by A40, CARD_3:def_5;
 f . (indx CC) in p by A41, A47;
then consider g being Function such that
A48: g in S and
A49: f . (indx CC) = g . (indx CC) by CARD_3:def_6;
reconsider g = g as ManySortedSet of I by A48;
A50: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in I implies f . b1 = g . b1 )
assume  i in I ; ::_thesis: f . b1 = g . b1
then reconsider j = i as Element of I ;
percases ( i = indx CC or i <> indx CC ) ;
suppose i = indx CC ; ::_thesis: f . b1 = g . b1
hence  f . i = g . i by A49; ::_thesis: verum
end;
supposeA51: i <> indx CC ; ::_thesis: f . b1 = g . b1
then  CC . j is 1 -element by Th12;
then consider c being set  such that
A52: CC . i = {c} by ZFMISC_1:131;
A53: g . j in CC . j by A13, A48, A51;
 f . j in B . j by A47;
then  f . j in {c} by A51, A52, FUNCT_7:32;
hence f . i = c by TARSKI:def_1
.= g . i by A52, A53, TARSKI:def_1 ;
::_thesis: verum
end;
end;
end;
 dom g = I by PARTFUN1:def_2;
hence  e in S by A46, A48, A50, FUNCT_1:2; ::_thesis: verum
end;
let SS be Subset of (A . (indx B)); ::_thesis: ( SS = B . (indx B) implies ( SS is strong & SS is closed_under_lines ) )
assume A54: SS = B . (indx B) ; ::_thesis: ( SS is strong & SS is closed_under_lines )
thus  SS is strong ::_thesis: SS is closed_under_lines
proof
let q, r be Point of (A . (indx B)); :: according to PENCIL_1:def_3 ::_thesis: ( q in SS & r in SS implies q,r are_collinear )
assume that
A55: q in SS and
A56: r in SS ; ::_thesis: q,r are_collinear
thus  q,r are_collinear ::_thesis: verum
proof
percases ( q = r or q <> r ) ;
suppose q = r ; ::_thesis: q,r are_collinear
hence  q,r are_collinear by Def1; ::_thesis: verum
end;
supposeA57: q <> r ; ::_thesis: q,r are_collinear
reconsider R = a1 +* ((indx B),r) as Point of (Segre_Product A) by Th25;
reconsider Q = a1 +* ((indx B),q) as Point of (Segre_Product A) by Th25;
reconsider Q1 = Q, R1 = R as ManySortedSet of I ;
A58: now__::_thesis:_not_Q_=_R
 dom a1 = I by PARTFUN1:def_2;
then A59: Q1 . (indx B) = q by FUNCT_7:31;
A60: dom a1 = I by PARTFUN1:def_2;
assume  Q = R ; ::_thesis: contradiction
hence  contradiction by A57, A59, A60, FUNCT_7:31; ::_thesis: verum
end;
A61: for i being set st i in dom B holds
Q1 . i in B . i
proof
let i be set ; ::_thesis: ( i in dom B implies Q1 . i in B . i )
assume A62: i in dom B ; ::_thesis: Q1 . i in B . i
then  i in I by PARTFUN1:def_2;
then A63: i in dom a1 by PARTFUN1:def_2;
percases ( i <> indx B or i = indx B ) ;
suppose i <> indx B ; ::_thesis: Q1 . i in B . i
then  Q1 . i = a1 . i by FUNCT_7:32;
hence  Q1 . i in B . i by A2, A42, A62, CARD_3:9; ::_thesis: verum
end;
suppose i = indx B ; ::_thesis: Q1 . i in B . i
hence  Q1 . i in B . i by A54, A55, A63, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
A64: for i being set st i in dom B holds
R1 . i in B . i
proof
let i be set ; ::_thesis: ( i in dom B implies R1 . i in B . i )
assume A65: i in dom B ; ::_thesis: R1 . i in B . i
then  i in I by PARTFUN1:def_2;
then A66: i in dom a1 by PARTFUN1:def_2;
percases ( i <> indx B or i = indx B ) ;
suppose i <> indx B ; ::_thesis: R1 . i in B . i
then  R1 . i = a1 . i by FUNCT_7:32;
hence  R1 . i in B . i by A2, A42, A65, CARD_3:9; ::_thesis: verum
end;
suppose i = indx B ; ::_thesis: R1 . i in B . i
hence  R1 . i in B . i by A54, A56, A66, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
dom R1 = I by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
then A67: R in product B by A64, CARD_3:9;
dom Q1 = I by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
then  Q in product B by A61, CARD_3:9;
then  Q,R are_collinear by A1, A42, A67, Def3;
then consider L being Block of (Segre_Product A) such that
A68: {Q,R} c= L by A58, Def1;
 dom a1 = I by PARTFUN1:def_2;
then A69: R1 . (indx B) = r by FUNCT_7:31;
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A70: L = product L1 and
A71: L1 . (indx L1) is Block of (A . (indx L1)) by Th24;
A72: dom L1 = I by PARTFUN1:def_2;
 Q1 in product L1 by A68, A70, ZFMISC_1:32;
then A73: Q1 . (indx B) in L1 . (indx B) by A72, CARD_3:9;
A74: dom L1 = I by PARTFUN1:def_2;
 R1 in product L1 by A68, A70, ZFMISC_1:32;
then A75: R1 . (indx B) in L1 . (indx B) by A74, CARD_3:9;
now__::_thesis:_not_Q1_._(indx_B)_=_R1_._(indx_B)
 dom a1 = I by PARTFUN1:def_2;
then A76: Q1 . (indx B) = q by FUNCT_7:31;
A77: dom a1 = I by PARTFUN1:def_2;
assume  Q1 . (indx B) = R1 . (indx B) ; ::_thesis: contradiction
hence  contradiction by A57, A76, A77, FUNCT_7:31; ::_thesis: verum
end;
then  2 c= card (L1 . (indx B)) by A73, A75, Th2;
then A78: not L1 . (indx B) is trivial by Th4;
then reconsider LI = L1 . (indx L1) as Block of (A . (indx B)) by A71, Def21;
 dom a1 = I by PARTFUN1:def_2;
then A79: Q1 . (indx B) = q by FUNCT_7:31;
 indx B = indx L1 by A78, Def21;
then  {q,r} c= LI by A73, A75, A79, A69, ZFMISC_1:32;
hence  q,r are_collinear by Def1; ::_thesis: verum
end;
end;
end;
end;
thus  SS is closed_under_lines ::_thesis: verum
proof
let L be Block of (A . (indx B)); :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (L /\ SS) implies L c= SS )
A80: dom B = I by PARTFUN1:def_2;
 2 c= card L by Def6;
then reconsider L1 = L as non trivial set by Th4;
 L in the topology of (A . (indx B)) ;
then A81: L c= the carrier of (A . (indx B)) ;
 B +* ((indx B),L1) c= Carrier A
proof
let o be set ; :: according to PBOOLE:def_2 ::_thesis: ( not o in I or (B +* ((indx B),L1)) . o c= (Carrier A) . o )
assume A82: o in I ; ::_thesis: (B +* ((indx B),L1)) . o c= (Carrier A) . o
thus  (B +* ((indx B),L1)) . o c= (Carrier A) . o ::_thesis: verum
proof
percases ( o <> indx B or o = indx B ) ;
supposeA83: o <> indx B ; ::_thesis: (B +* ((indx B),L1)) . o c= (Carrier A) . o
A84: B c= Carrier A by PBOOLE:def_18;
 (B +* ((indx B),L1)) . o = B . o by A83, FUNCT_7:32;
hence  (B +* ((indx B),L1)) . o c= (Carrier A) . o by A82, A84, PBOOLE:def_2; ::_thesis: verum
end;
supposeA85: o = indx B ; ::_thesis: (B +* ((indx B),L1)) . o c= (Carrier A) . o
then  (B +* ((indx B),L1)) . o = L by A40, FUNCT_7:31;
hence  (B +* ((indx B),L1)) . o c= (Carrier A) . o by A81, A85, YELLOW_6:2; ::_thesis: verum
end;
end;
end;
end;
then reconsider L2 = B +* ((indx B),L1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th27, PBOOLE:def_18;
A86: L2 . (indx B) = L1 by A40, FUNCT_7:31;
then  indx B = indx L2 by Def21;
then  L2 . (indx L2) is Block of (A . (indx L2)) by A80, FUNCT_7:31;
then reconsider L3 = product L2 as Block of (Segre_Product A) by Th24;
assume  2 c= card (L /\ SS) ; ::_thesis: L c= SS
then consider x, y being set  such that
A87: x in L /\ SS and
A88: y in L /\ SS and
A89: x <> y by Th2;
set y1 = a1 +* ((indx B),y);
A90: dom (a1 +* ((indx B),y)) = I by PARTFUN1:def_2;
now__::_thesis:_for_o_being_set_st_o_in_I_holds_
(a1_+*_((indx_B),y))_._o_in_B_._o
let o be set ; ::_thesis: ( o in I implies (a1 +* ((indx B),y)) . b1 in B . b1 )
assume A91: o in I ; ::_thesis: (a1 +* ((indx B),y)) . b1 in B . b1
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in B . b1
then  (a1 +* ((indx B),y)) . o = a1 . o by FUNCT_7:32;
hence  (a1 +* ((indx B),y)) . o in B . o by A2, A40, A42, A91, CARD_3:9; ::_thesis: verum
end;
supposeA92: o = indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in B . b1
then  (a1 +* ((indx B),y)) . o = y by A8, FUNCT_7:31;
hence  (a1 +* ((indx B),y)) . o in B . o by A54, A88, A92, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then A93: a1 +* ((indx B),y) in S by A40, A42, A90, CARD_3:9;
A94: dom L2 = I by PARTFUN1:def_2;
now__::_thesis:_for_o_being_set_st_o_in_dom_L2_holds_
(a1_+*_((indx_B),y))_._o_in_L2_._o
let o be set ; ::_thesis: ( o in dom L2 implies (a1 +* ((indx B),y)) . b1 in L2 . b1 )
assume A95: o in dom L2 ; ::_thesis: (a1 +* ((indx B),y)) . b1 in L2 . b1
percases ( o <> indx B or o = indx B ) ;
supposeA96: o <> indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in L2 . b1
then A97: (a1 +* ((indx B),y)) . o = a1 . o by FUNCT_7:32;
 a1 . o in B . o by A2, A40, A42, A94, A95, CARD_3:9;
hence  (a1 +* ((indx B),y)) . o in L2 . o by A96, A97, FUNCT_7:32; ::_thesis: verum
end;
supposeA98: o = indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in L2 . b1
then  (a1 +* ((indx B),y)) . o = y by A8, FUNCT_7:31;
hence  (a1 +* ((indx B),y)) . o in L2 . o by A88, A86, A98, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then  a1 +* ((indx B),y) in L3 by A94, A90, CARD_3:9;
then A99: a1 +* ((indx B),y) in L3 /\ S by A93, XBOOLE_0:def_4;
set x1 = a1 +* ((indx B),x);
A100: dom (a1 +* ((indx B),x)) = I by PARTFUN1:def_2;
now__::_thesis:_for_o_being_set_st_o_in_I_holds_
(a1_+*_((indx_B),x))_._o_in_B_._o
let o be set ; ::_thesis: ( o in I implies (a1 +* ((indx B),x)) . b1 in B . b1 )
assume A101: o in I ; ::_thesis: (a1 +* ((indx B),x)) . b1 in B . b1
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in B . b1
then  (a1 +* ((indx B),x)) . o = a1 . o by FUNCT_7:32;
hence  (a1 +* ((indx B),x)) . o in B . o by A2, A40, A42, A101, CARD_3:9; ::_thesis: verum
end;
supposeA102: o = indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in B . b1
then  (a1 +* ((indx B),x)) . o = x by A8, FUNCT_7:31;
hence  (a1 +* ((indx B),x)) . o in B . o by A54, A87, A102, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then A103: a1 +* ((indx B),x) in S by A40, A42, A100, CARD_3:9;
A104: ( (a1 +* ((indx B),x)) . (indx B) = x & (a1 +* ((indx B),y)) . (indx B) = y ) by A8, FUNCT_7:31;
now__::_thesis:_for_o_being_set_st_o_in_dom_L2_holds_
(a1_+*_((indx_B),x))_._o_in_L2_._o
let o be set ; ::_thesis: ( o in dom L2 implies (a1 +* ((indx B),x)) . b1 in L2 . b1 )
assume A105: o in dom L2 ; ::_thesis: (a1 +* ((indx B),x)) . b1 in L2 . b1
percases ( o <> indx B or o = indx B ) ;
supposeA106: o <> indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in L2 . b1
then A107: (a1 +* ((indx B),x)) . o = a1 . o by FUNCT_7:32;
 a1 . o in B . o by A2, A40, A42, A94, A105, CARD_3:9;
hence  (a1 +* ((indx B),x)) . o in L2 . o by A106, A107, FUNCT_7:32; ::_thesis: verum
end;
supposeA108: o = indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in L2 . b1
then  (a1 +* ((indx B),x)) . o = x by A8, FUNCT_7:31;
hence  (a1 +* ((indx B),x)) . o in L2 . o by A87, A86, A108, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then  a1 +* ((indx B),x) in L3 by A94, A100, CARD_3:9;
then  a1 +* ((indx B),x) in L3 /\ S by A103, XBOOLE_0:def_4;
then  2 c= card (L3 /\ S) by A89, A104, A99, Th2;
then A109: L3 c= S by A1, Def2;
thus  L c= SS ::_thesis: verum
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in L or e in SS )
consider f being set  such that
A110: f in L3 by XBOOLE_0:def_1;
A111: ex F being Function st
( F = f & dom F = I & ( for o being set st o in I holds
F . o in L2 . o ) ) by A94, A110, CARD_3:def_5;
then reconsider f = f as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
assume A112: e in L ; ::_thesis: e in SS
A113: now__::_thesis:_for_o_being_set_st_o_in_dom_L2_holds_
(f_+*_((indx_B),e))_._o_in_L2_._o
let o be set ; ::_thesis: ( o in dom L2 implies (f +* ((indx B),e)) . b1 in L2 . b1 )
assume A114: o in dom L2 ; ::_thesis: (f +* ((indx B),e)) . b1 in L2 . b1
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: (f +* ((indx B),e)) . b1 in L2 . b1
then  (f +* ((indx B),e)) . o = f . o by FUNCT_7:32;
hence  (f +* ((indx B),e)) . o in L2 . o by A94, A111, A114; ::_thesis: verum
end;
supposeA115: o = indx B ; ::_thesis: (f +* ((indx B),e)) . b1 in L2 . b1
then  (f +* ((indx B),e)) . o = e by A111, FUNCT_7:31;
hence  (f +* ((indx B),e)) . o in L2 . o by A40, A112, A115, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
 dom (f +* ((indx B),e)) = dom L2 by A94, PARTFUN1:def_2;
then  f +* ((indx B),e) in L3 by A113, CARD_3:9;
then  (f +* ((indx B),e)) . (indx B) in B . (indx B) by A40, A42, A109, CARD_3:9;
hence  e in SS by A54, A111, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
given B being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A116: S = product B and
A117: for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ; ::_thesis: ( not S is trivial & S is strong & S is closed_under_lines )
thus  not S is trivial by A116; ::_thesis: ( S is strong & S is closed_under_lines )
A118: dom B = I by PARTFUN1:def_2;
A119: dom (Carrier A) = I by PARTFUN1:def_2;
thus  S is strong ::_thesis: S is closed_under_lines
proof
let x, y be Point of (Segre_Product A); :: according to PENCIL_1:def_3 ::_thesis: ( x in S & y in S implies x,y are_collinear )
assume that
A120: x in S and
A121: y in S ; ::_thesis: x,y are_collinear
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: x,y are_collinear
hence  x,y are_collinear by Def1; ::_thesis: verum
end;
supposeA122: x <> y ; ::_thesis: x,y are_collinear
consider y1 being Function such that
A123: y1 = y and
A124: dom y1 = dom (Carrier A) and
A125: for a being set st a in dom (Carrier A) holds
y1 . a in (Carrier A) . a by CARD_3:def_5;
A126: dom (Carrier A) = I by PARTFUN1:def_2;
then reconsider y1 = y1 as ManySortedSet of I by A124, PARTFUN1:def_2, RELAT_1:def_18;
consider x1 being Function such that
A127: x1 = x and
A128: dom x1 = dom (Carrier A) and
A129: for a being set st a in dom (Carrier A) holds
x1 . a in (Carrier A) . a by CARD_3:def_5;
reconsider x1 = x1 as ManySortedSet of I by A128, A126, PARTFUN1:def_2, RELAT_1:def_18;
A130: now__::_thesis:_not_x1_._(indx_B)_=_y1_._(indx_B)
assume A131: x1 . (indx B) = y1 . (indx B) ; ::_thesis: contradiction
now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_
x1_._i_=_y1_._i
let i be set ; ::_thesis: ( i in dom (Carrier A) implies x1 . b1 = y1 . b1 )
assume  i in dom (Carrier A) ; ::_thesis: x1 . b1 = y1 . b1
percases ( i <> indx B or i = indx B ) ;
suppose i <> indx B ; ::_thesis: x1 . b1 = y1 . b1
hence  x1 . i = y1 . i by A116, A120, A121, A127, A123, Th23; ::_thesis: verum
end;
suppose i = indx B ; ::_thesis: x1 . b1 = y1 . b1
hence  x1 . i = y1 . i by A131; ::_thesis: verum
end;
end;
end;
hence  contradiction by A122, A127, A128, A123, A124, FUNCT_1:2; ::_thesis: verum
end;
 B c= Carrier A by PBOOLE:def_18;
then  B . (indx B) c= (Carrier A) . (indx B) by PBOOLE:def_2;
then reconsider C = B . (indx B) as Subset of (A . (indx B)) by YELLOW_6:2;
A132: C is strong by A117;
 y1 . (indx B) in (Carrier A) . (indx B) by A119, A125;
then reconsider y1i = y1 . (indx B) as Point of (A . (indx B)) by YELLOW_6:2;
A133: y1i in C by A116, A118, A121, A123, CARD_3:9;
 x1 . (indx B) in (Carrier A) . (indx B) by A119, A129;
then reconsider x1i = x1 . (indx B) as Point of (A . (indx B)) by YELLOW_6:2;
 x1i in C by A116, A118, A120, A127, CARD_3:9;
then  x1i,y1i are_collinear by A133, A132, Def3;
then consider l being Block of (A . (indx B)) such that
A134: {x1i,y1i} c= l by A130, Def1;
A135: dom {x1} = I by PARTFUN1:def_2;
A136: for a being set st a in dom ({x1} +* ((indx B),l)) holds
y1 . a in ({x1} +* ((indx B),l)) . a
proof
let a be set ; ::_thesis: ( a in dom ({x1} +* ((indx B),l)) implies y1 . a in ({x1} +* ((indx B),l)) . a )
assume  a in dom ({x1} +* ((indx B),l)) ; ::_thesis: y1 . a in ({x1} +* ((indx B),l)) . a
then A137: a in I by PARTFUN1:def_2;
percases ( a = indx B or a <> indx B ) ;
supposeA138: a = indx B ; ::_thesis: y1 . a in ({x1} +* ((indx B),l)) . a
then  ({x1} +* ((indx B),l)) . a = l by A135, FUNCT_7:31;
hence  y1 . a in ({x1} +* ((indx B),l)) . a by A134, A138, ZFMISC_1:32; ::_thesis: verum
end;
supposeA139: a <> indx B ; ::_thesis: y1 . a in ({x1} +* ((indx B),l)) . a
 x1 . a in {(x1 . a)} by TARSKI:def_1;
then  x1 . a in {x1} . a by A137, PZFMISC1:def_1;
then  y1 . a in {x1} . a by A116, A120, A121, A127, A123, A139, Th23;
hence  y1 . a in ({x1} +* ((indx B),l)) . a by A139, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
 {x1} +* ((indx B),l) c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ({x1} +* ((indx B),l)) . i c= (Carrier A) . i )
assume A140: i in I ; ::_thesis: ({x1} +* ((indx B),l)) . i c= (Carrier A) . i
then reconsider i1 = i as Element of I ;
thus  ({x1} +* ((indx B),l)) . i c= (Carrier A) . i ::_thesis: verum
proof
percases ( i = indx B or i <> indx B ) ;
supposeA141: i = indx B ; ::_thesis: ({x1} +* ((indx B),l)) . i c= (Carrier A) . i
then  ({x1} +* ((indx B),l)) . i = l by A135, FUNCT_7:31;
then  ({x1} +* ((indx B),l)) . i in the topology of (A . (indx B)) ;
then  ({x1} +* ((indx B),l)) . i c= the carrier of (A . (indx B)) ;
hence  ({x1} +* ((indx B),l)) . i c= (Carrier A) . i by A141, YELLOW_6:2; ::_thesis: verum
end;
supposeA142: i <> indx B ; ::_thesis: ({x1} +* ((indx B),l)) . i c= (Carrier A) . i
 x1 . i in (Carrier A) . i1 by A119, A129;
then  x1 . i in the carrier of (A . i1) by YELLOW_6:2;
then A143: {(x1 . i)} c= the carrier of (A . i1) by ZFMISC_1:31;
({x1} +* ((indx B),l)) . i = {x1} . i by A142, FUNCT_7:32
.= {(x1 . i)} by A140, PZFMISC1:def_1 ;
hence  ({x1} +* ((indx B),l)) . i c= (Carrier A) . i by A143, YELLOW_6:2; ::_thesis: verum
end;
end;
end;
end;
then A144: {x1} +* ((indx B),l) is ManySortedSubset of Carrier A by PBOOLE:def_18;
 for i being Element of I st i <> indx B holds
({x1} +* ((indx B),l)) . i is 1 -element
proof
let i be Element of I; ::_thesis: ( i <> indx B implies ({x1} +* ((indx B),l)) . i is 1 -element )
assume  i <> indx B ; ::_thesis: ({x1} +* ((indx B),l)) . i is 1 -element
then ({x1} +* ((indx B),l)) . i = {x1} . i by FUNCT_7:32
.= {(x1 . i)} by PZFMISC1:def_1 ;
hence  ({x1} +* ((indx B),l)) . i is 1 -element ; ::_thesis: verum
end;
then A145: {x1} +* ((indx B),l) is Segre-like by Def20;
A146: for a being set st a in dom ({x1} +* ((indx B),l)) holds
x1 . a in ({x1} +* ((indx B),l)) . a
proof
let a be set ; ::_thesis: ( a in dom ({x1} +* ((indx B),l)) implies x1 . a in ({x1} +* ((indx B),l)) . a )
assume  a in dom ({x1} +* ((indx B),l)) ; ::_thesis: x1 . a in ({x1} +* ((indx B),l)) . a
then A147: a in I by PARTFUN1:def_2;
percases ( a = indx B or a <> indx B ) ;
supposeA148: a = indx B ; ::_thesis: x1 . a in ({x1} +* ((indx B),l)) . a
then  ({x1} +* ((indx B),l)) . a = l by A135, FUNCT_7:31;
hence  x1 . a in ({x1} +* ((indx B),l)) . a by A134, A148, ZFMISC_1:32; ::_thesis: verum
end;
supposeA149: a <> indx B ; ::_thesis: x1 . a in ({x1} +* ((indx B),l)) . a
 x1 . a in {(x1 . a)} by TARSKI:def_1;
then  x1 . a in {x1} . a by A147, PZFMISC1:def_1;
hence  x1 . a in ({x1} +* ((indx B),l)) . a by A149, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
 ({x1} +* ((indx B),l)) . (indx B) is Block of (A . (indx B)) by A135, FUNCT_7:31;
then reconsider L = product ({x1} +* ((indx B),l)) as Block of (Segre_Product A) by A145, A144, Def22;
dom y1 = I by PARTFUN1:def_2
.= dom ({x1} +* ((indx B),l)) by PARTFUN1:def_2 ;
then A150: y1 in L by A136, CARD_3:9;
dom x1 = I by PARTFUN1:def_2
.= dom ({x1} +* ((indx B),l)) by PARTFUN1:def_2 ;
then  x1 in L by A146, CARD_3:9;
then  {x,y} c= L by A127, A123, A150, ZFMISC_1:32;
hence  x,y are_collinear by Def1; ::_thesis: verum
end;
end;
end;
thus  S is closed_under_lines ::_thesis: verum
proof
let l be Block of (Segre_Product A); :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (l /\ S) implies l c= S )
consider L being Segre-like ManySortedSubset of Carrier A such that
A151: l = product L and
A152: ex i being Element of I st L . i is Block of (A . i) by Def22;
assume A153: 2 c= card (l /\ S) ; ::_thesis: l c= S
then consider a, b being set  such that
A154: a in l /\ S and
A155: b in l /\ S and
A156: a <> b by Th2;
 card (l /\ S) c= card l by CARD_1:11, XBOOLE_1:17;
then  2 c= card l by A153, XBOOLE_1:1;
then reconsider L = L as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A151, Th13;
reconsider a1 = a, b1 = b as ManySortedSet of I by A154, A155, Th14;
A157: dom L = I by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
A158: indx B = indx L by A116, A153, A151, Th26;
 for a being set st a in dom L holds
L . a c= B . a
proof
let a be set ; ::_thesis: ( a in dom L implies L . a c= B . a )
assume  a in dom L ; ::_thesis: L . a c= B . a
percases ( a <> indx B or a = indx B ) ;
suppose a <> indx B ; ::_thesis: L . a c= B . a
hence  L . a c= B . a by A116, A153, A151, Th26; ::_thesis: verum
end;
supposeA159: a = indx B ; ::_thesis: L . a c= B . a
 B c= Carrier A by PBOOLE:def_18;
then  B . (indx B) c= (Carrier A) . (indx B) by PBOOLE:def_2;
then reconsider C = B . (indx B) as Subset of (A . (indx B)) by YELLOW_6:2;
consider j being Element of I such that
A160: L . j is Block of (A . j) by A152;
 2 c= card (L . j) by A160, Def6;
then  not L . j is trivial by Th4;
then  j = indx L by Def21;
then reconsider Li = L . (indx B) as Block of (A . (indx B)) by A158, A160;
A161: C is closed_under_lines by A117;
 a1 in product L by A154, A151, XBOOLE_0:def_4;
then A162: a1 . (indx B) in L . (indx B) by A118, A157, CARD_3:9;
 b1 in product L by A155, A151, XBOOLE_0:def_4;
then A163: b1 . (indx B) in L . (indx B) by A118, A157, CARD_3:9;
A164: b1 in product B by A116, A155, XBOOLE_0:def_4;
then  b1 . (indx B) in B . (indx B) by A118, CARD_3:9;
then A165: b1 . (indx B) in Li /\ C by A163, XBOOLE_0:def_4;
A166: a1 in product B by A116, A154, XBOOLE_0:def_4;
A167: now__::_thesis:_not_a1_._(indx_B)_=_b1_._(indx_B)
assume A168: a1 . (indx B) = b1 . (indx B) ; ::_thesis: contradiction
A169: for o being set st o in dom a1 holds
a1 . o = b1 . o
proof
let o be set ; ::_thesis: ( o in dom a1 implies a1 . o = b1 . o )
assume  o in dom a1 ; ::_thesis: a1 . o = b1 . o
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: a1 . o = b1 . o
hence  a1 . o = b1 . o by A166, A164, Th23; ::_thesis: verum
end;
suppose o = indx B ; ::_thesis: a1 . o = b1 . o
hence  a1 . o = b1 . o by A168; ::_thesis: verum
end;
end;
end;
dom a1 = I by PARTFUN1:def_2
.= dom b1 by PARTFUN1:def_2 ;
hence  contradiction by A156, A169, FUNCT_1:2; ::_thesis: verum
end;
 a1 . (indx B) in B . (indx B) by A118, A166, CARD_3:9;
then  a1 . (indx B) in Li /\ C by A162, XBOOLE_0:def_4;
then  2 c= card (Li /\ C) by A167, A165, Th2;
hence  L . a c= B . a by A159, A161, Def2; ::_thesis: verum
end;
end;
end;
hence  l c= S by A116, A151, A157, CARD_3:27; ::_thesis: verum
end;
end;