let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
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 ; :: 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 ) ) ) )
A1: dom (Carrier A) = I by PARTFUN1:def 4;
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 A2: ( 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
A3: ( a in S & b in S & a <> b ) by Th2;
reconsider a = a, b = b as Point of (Segre_Product A) by A3;
reconsider a1 = a, b1 = b as ManySortedSet of by Th14;
A4: ( dom a1 = I & dom b1 = I ) by PARTFUN1:def 4;
a,b are_collinear by A2, A3, Def3;
then consider C being Block of (Segre_Product A) such that
A5: {a,b} c= C by A3, Def1;
consider CC being Segre-like ManySortedSubset of Carrier A such that
A6: ( C = product CC & 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:38;
then 2 c= card (product CC) by A3, Th2;
then reconsider CC = CC as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th13;
A7: ( a1 . (indx CC) in pi S,(indx CC) & b1 . (indx CC) in pi S,(indx CC) ) by A3, CARD_3:def 6;

A8: now

assume A9: 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

per cases ( i = indx CC or i <> indx CC ) ;

suppose i = indx CC ; :: thesis: a1 . i = b1 . i

hence a1 . i = b1 . i by A9; :: thesis: verum

end;

suppose A10: i <> indx CC ; :: thesis: a1 . i = b1 . i

( a1 in product CC & b1 in product CC ) by A5, A6, ZFMISC_1:38;
hence a1 . i = b1 . i by A10, Th23; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A4, FUNCT_1:9; :: thesis: verum

end;

then 2 c= card (pi S,(indx CC)) by A7, 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 5 :: thesis: ( not i in I or (CC +* (indx CC),p) . i c= (Carrier A) . i )
assume A11: i in I ; :: thesis: (CC +* (indx CC),p) . i c= (Carrier A) . i

per cases ( i <> indx CC or i = indx CC ) ;

suppose i <> indx CC ; :: thesis: (CC +* (indx CC),p) . i c= (Carrier A) . i

then A12: (CC +* (indx CC),p) . i = CC . i by FUNCT_7:34;
CC c= Carrier A by PBOOLE:def 23;
hence (CC +* (indx CC),p) . i c= (Carrier A) . i by A11, A12, PBOOLE:def 5; :: thesis: verum

end;

suppose A13: i = indx CC ; :: thesis: (CC +* (indx CC),p) . i c= (Carrier A) . i

A14: dom CC = I by PARTFUN1:def 4;
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 consider f being Function such that
A15: ( f in S & y = f . i ) by A13, CARD_3:def 6;
i in dom (Carrier A) by A11, PARTFUN1:def 4;
hence y in (Carrier A) . i by A15, CARD_3:18; :: thesis: verum

end;

hence (CC +* (indx CC),p) . i c= (Carrier A) . i by A13, A14, FUNCT_7:33; :: 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 23;
A16: dom CC = I by PARTFUN1:def 4;
then A17: B . (indx CC) = p by FUNCT_7:33;
A18: dom B = I by PARTFUN1:def 4;
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 ) ) )
A19: for f being ManySortedSet of 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 ; :: thesis: ( f in S implies for i being Element of I st i <> indx CC holds
f . i in CC . i )
assume A20: 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 A21: i <> indx CC ; :: thesis: f . i in CC . i

now

assume A22: not f . i in CC . i ; :: thesis: contradiction
a1 in product CC by A5, A6, ZFMISC_1:38;
then A23: a1 . i in CC . i by A16, CARD_3:18;
b1 in product CC by A5, A6, ZFMISC_1:38;
then A24: b1 . i in CC . i by A16, CARD_3:18;
f1,a are_collinear by A2, A3, A20, Def3;
then consider la being Block of (Segre_Product A) such that
A25: {f1,a} c= la by A22, A23, Def1;
consider La being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A26: ( la = product La & La . (indx La) is Block of (A . (indx La)) ) by Th24;
A27: ( f in product La & a1 in product La ) by A25, A26, ZFMISC_1:38;
then indx La = i by A22, A23, Th23;
then ( not La . (indx CC) is empty & La . (indx CC) is trivial ) by A21, Th12;
then consider ca being set such that
A28: La . (indx CC) = {ca} by REALSET1:def 4;
dom La = I by PARTFUN1:def 4;
then A29: ( a1 . (indx CC) in {ca} & f . (indx CC) in {ca} ) by A27, A28, CARD_3:18;
f1,b are_collinear by A2, A3, A20, Def3;
then consider lb being Block of (Segre_Product A) such that
A30: {f1,b} c= lb by A22, A24, Def1;
consider Lb being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A31: ( lb = product Lb & Lb . (indx Lb) is Block of (A . (indx Lb)) ) by Th24;
A32: ( f in product Lb & b1 in product Lb ) by A30, A31, ZFMISC_1:38;
then indx Lb = i by A22, A24, Th23;
then ( not Lb . (indx CC) is empty & Lb . (indx CC) is trivial ) by A21, Th12;
then consider cb being set such that
A33: Lb . (indx CC) = {cb} by REALSET1:def 4;
dom Lb = I by PARTFUN1:def 4;
then A34: ( b1 . (indx CC) in {cb} & f . (indx CC) in {cb} ) by A32, A33, CARD_3:18;
then b1 . (indx CC) = cb by TARSKI:def 1;
then ca <> cb by A8, A29, TARSKI:def 1;
then f . (indx CC) <> cb by A29, TARSKI:def 1;
hence contradiction by A34, TARSKI:def 1; :: thesis: verum

end;

hence f . i in CC . i ; :: thesis: verum

end;

thus A35: 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 A36: e in S ; :: thesis: e in product B
then reconsider f = e as ManySortedSet of by Th14;
A37: dom f = I by PARTFUN1:def 4;

now

let i be set ; :: thesis: ( i in I implies f . b₁ in B . b₁ )
assume i in I ; :: thesis: f . b₁ in B . b₁
then reconsider j = i as Element of I ;

per cases ( j = indx CC or j <> indx CC ) ;

suppose j = indx CC ; :: thesis: f . b₁ in B . b₁

hence f . i in B . i by A17, A36, CARD_3:def 6; :: thesis: verum

end;

suppose A38: j <> indx CC ; :: thesis: f . b₁ in B . b₁

then f . j in CC . j by A19, A36;
hence f . i in B . i by A38, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence e in product B by A18, A37, CARD_3:18; :: 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
A39: ( e = f & dom f = I & ( for i being set st i in I holds
f . i in B . i ) ) by A18, CARD_3:def 5;
f . (indx CC) in p by A17, A39;
then consider g being Function such that
A40: ( g in S & f . (indx CC) = g . (indx CC) ) by CARD_3:def 6;
reconsider g = g as ManySortedSet of by A40, Th14;
A41: dom g = I by PARTFUN1:def 4;

now

let i be set ; :: thesis: ( i in I implies f . b₁ = g . b₁ )
assume i in I ; :: thesis: f . b₁ = g . b₁
then reconsider j = i as Element of I ;

per cases ( i = indx CC or i <> indx CC ) ;

suppose i = indx CC ; :: thesis: f . b₁ = g . b₁

hence f . i = g . i by A40; :: thesis: verum

end;

suppose A42: i <> indx CC ; :: thesis: f . b₁ = g . b₁

then ( not CC . j is empty & CC . j is trivial ) by Th12;
then consider c being set such that
A43: CC . i = {c} by REALSET1:def 4;
A44: g . j in CC . j by A19, A40, A42;
f . j in B . j by A39;
then f . j in {c} by A42, A43, FUNCT_7:34;
hence f . i = c by TARSKI:def 1
.= g . i by A43, A44, TARSKI:def 1 ;
:: thesis: verum

end;

end;

end;

hence e in S by A39, A40, A41, FUNCT_1:9; :: 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 A45: 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 A46: ( q in SS & r in SS ) ; :: thesis: q,r are_collinear
thus q,r are_collinear :: thesis: verum

proof

per cases ( q = r or q <> r ) ;

suppose q = r ; :: thesis: q,r are_collinear

hence q,r are_collinear by Def1; :: thesis: verum

end;

suppose A47: q <> r ; :: thesis: q,r are_collinear

reconsider Q = a1 +* (indx B),q as Point of (Segre_Product A) by Th25;
reconsider R = a1 +* (indx B),r as Point of (Segre_Product A) by Th25;
reconsider Q1 = Q, R1 = R as ManySortedSet of ;
A48: dom Q1 = I by PARTFUN1:def 4
.= dom B by PARTFUN1:def 4 ;
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 A49: i in dom B ; :: thesis: Q1 . i in B . i
then i in I by PARTFUN1:def 4;
then A50: i in dom a1 by PARTFUN1:def 4;

per cases ( 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:34;
hence Q1 . i in B . i by A3, A35, A49, CARD_3:18; :: thesis: verum

end;

suppose i = indx B ; :: thesis: Q1 . i in B . i

hence Q1 . i in B . i by A45, A46, A50, FUNCT_7:33; :: thesis: verum

end;

end;

end;

then A51: Q in product B by A48, CARD_3:18;
A52: dom R1 = I by PARTFUN1:def 4
.= dom B by PARTFUN1:def 4 ;
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 A53: i in dom B ; :: thesis: R1 . i in B . i
then i in I by PARTFUN1:def 4;
then A54: i in dom a1 by PARTFUN1:def 4;

per cases ( 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:34;
hence R1 . i in B . i by A3, A35, A53, CARD_3:18; :: thesis: verum

end;

suppose i = indx B ; :: thesis: R1 . i in B . i

hence R1 . i in B . i by A45, A46, A54, FUNCT_7:33; :: thesis: verum

end;

end;

end;

then R in product B by A52, CARD_3:18;
then A55: Q,R are_collinear by A2, A35, A51, Def3;

now

assume A56: Q = R ; :: thesis: contradiction
dom a1 = I by PARTFUN1:def 4;
then A57: Q1 . (indx B) = q by FUNCT_7:33;
dom a1 = I by PARTFUN1:def 4;
hence contradiction by A47, A56, A57, FUNCT_7:33; :: thesis: verum

end;

then consider L being Block of (Segre_Product A) such that
A58: {Q,R} c= L by A55, Def1;
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A59: ( L = product L1 & L1 . (indx L1) is Block of (A . (indx L1)) ) by Th24;
A60: Q1 in product L1 by A58, A59, ZFMISC_1:38;
dom L1 = I by PARTFUN1:def 4;
then A61: Q1 . (indx B) in L1 . (indx B) by A60, CARD_3:18;
A62: R1 in product L1 by A58, A59, ZFMISC_1:38;
dom L1 = I by PARTFUN1:def 4;
then A63: R1 . (indx B) in L1 . (indx B) by A62, CARD_3:18;

now

assume A64: Q1 . (indx B) = R1 . (indx B) ; :: thesis: contradiction
dom a1 = I by PARTFUN1:def 4;
then A65: Q1 . (indx B) = q by FUNCT_7:33;
dom a1 = I by PARTFUN1:def 4;
hence contradiction by A47, A64, A65, FUNCT_7:33; :: thesis: verum

end;

then 2 c= card (L1 . (indx B)) by A61, A63, Th2;
then A66: not L1 . (indx B) is trivial by Th4;
then A67: indx B = indx L1 by Def21;
reconsider LI = L1 . (indx L1) as Block of (A . (indx B)) by A59, A66, Def21;
dom a1 = I by PARTFUN1:def 4;
then A68: Q1 . (indx B) = q by FUNCT_7:33;
dom a1 = I by PARTFUN1:def 4;
then R1 . (indx B) = r by FUNCT_7:33;
then {q,r} c= LI by A61, A63, A67, A68, ZFMISC_1:38;
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 )
L in the topology of (A . (indx B)) ;
then A69: L c= the carrier of (A . (indx B)) ;
assume 2 c= card (L /\ SS) ; :: thesis: L c= SS
then consider x, y being set such that
A70: ( x in L /\ SS & y in L /\ SS & x <> y ) by Th2;
2 c= card L by Def6;
then reconsider L1 = L as non trivial set by Th4;
set x1 = a1 +* (indx B),x;
set y1 = a1 +* (indx B),y;
A71: ( (a1 +* (indx B),x) . (indx B) = x & (a1 +* (indx B),y) . (indx B) = y ) by A4, FUNCT_7:33;
B +* (indx B),L1 c= Carrier A

proof

let o be set ; :: according to PBOOLE:def 5 :: thesis: ( not o in I or (B +* (indx B),L1) . o c= (Carrier A) . o )
assume A72: 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

per cases ( o <> indx B or o = indx B ) ;

suppose o <> indx B ; :: thesis: (B +* (indx B),L1) . o c= (Carrier A) . o

then A73: (B +* (indx B),L1) . o = B . o by FUNCT_7:34;
B c= Carrier A by PBOOLE:def 23;
hence (B +* (indx B),L1) . o c= (Carrier A) . o by A72, A73, PBOOLE:def 5; :: thesis: verum

end;

suppose A74: o = indx B ; :: thesis: (B +* (indx B),L1) . o c= (Carrier A) . o

then (B +* (indx B),L1) . o = L by A18, FUNCT_7:33;
hence (B +* (indx B),L1) . o c= (Carrier A) . o by A69, A74, YELLOW_6:9; :: 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 23;
A75: dom L2 = I by PARTFUN1:def 4;
A76: L2 . (indx B) = L1 by A18, FUNCT_7:33;
then A77: indx B = indx L2 by Def21;
dom B = I by PARTFUN1:def 4;
then L2 . (indx L2) is Block of (A . (indx L2)) by A77, FUNCT_7:33;
then reconsider L3 = product L2 as Block of (Segre_Product A) by Th24;
A78: dom (a1 +* (indx B),x) = I by PARTFUN1:def 4;

now

let o be set ; :: thesis: ( o in dom L2 implies (a1 +* (indx B),x) . b₁ in L2 . b₁ )
assume A79: o in dom L2 ; :: thesis: (a1 +* (indx B),x) . b₁ in L2 . b₁

per cases ( o <> indx B or o = indx B ) ;

suppose A80: o <> indx B ; :: thesis: (a1 +* (indx B),x) . b₁ in L2 . b₁

then A81: (a1 +* (indx B),x) . o = a1 . o by FUNCT_7:34;
a1 . o in B . o by A3, A18, A35, A75, A79, CARD_3:18;
hence (a1 +* (indx B),x) . o in L2 . o by A80, A81, FUNCT_7:34; :: thesis: verum

end;

suppose A82: o = indx B ; :: thesis: (a1 +* (indx B),x) . b₁ in L2 . b₁

then (a1 +* (indx B),x) . o = x by A4, FUNCT_7:33;
hence (a1 +* (indx B),x) . o in L2 . o by A70, A76, A82, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then A83: a1 +* (indx B),x in L3 by A75, A78, CARD_3:18;

now

let o be set ; :: thesis: ( o in I implies (a1 +* (indx B),x) . b₁ in B . b₁ )
assume A84: o in I ; :: thesis: (a1 +* (indx B),x) . b₁ in B . b₁

per cases ( o <> indx B or o = indx B ) ;

suppose o <> indx B ; :: thesis: (a1 +* (indx B),x) . b₁ in B . b₁

then (a1 +* (indx B),x) . o = a1 . o by FUNCT_7:34;
hence (a1 +* (indx B),x) . o in B . o by A3, A18, A35, A84, CARD_3:18; :: thesis: verum

end;

suppose A85: o = indx B ; :: thesis: (a1 +* (indx B),x) . b₁ in B . b₁

then (a1 +* (indx B),x) . o = x by A4, FUNCT_7:33;
hence (a1 +* (indx B),x) . o in B . o by A45, A70, A85, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then a1 +* (indx B),x in S by A18, A35, A78, CARD_3:18;
then A86: a1 +* (indx B),x in L3 /\ S by A83, XBOOLE_0:def 4;
A87: dom (a1 +* (indx B),y) = I by PARTFUN1:def 4;

now

let o be set ; :: thesis: ( o in dom L2 implies (a1 +* (indx B),y) . b₁ in L2 . b₁ )
assume A88: o in dom L2 ; :: thesis: (a1 +* (indx B),y) . b₁ in L2 . b₁

per cases ( o <> indx B or o = indx B ) ;

suppose A89: o <> indx B ; :: thesis: (a1 +* (indx B),y) . b₁ in L2 . b₁

then A90: (a1 +* (indx B),y) . o = a1 . o by FUNCT_7:34;
a1 . o in B . o by A3, A18, A35, A75, A88, CARD_3:18;
hence (a1 +* (indx B),y) . o in L2 . o by A89, A90, FUNCT_7:34; :: thesis: verum

end;

suppose A91: o = indx B ; :: thesis: (a1 +* (indx B),y) . b₁ in L2 . b₁

then (a1 +* (indx B),y) . o = y by A4, FUNCT_7:33;
hence (a1 +* (indx B),y) . o in L2 . o by A70, A76, A91, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then A92: a1 +* (indx B),y in L3 by A75, A87, CARD_3:18;

now

let o be set ; :: thesis: ( o in I implies (a1 +* (indx B),y) . b₁ in B . b₁ )
assume A93: o in I ; :: thesis: (a1 +* (indx B),y) . b₁ in B . b₁

per cases ( o <> indx B or o = indx B ) ;

suppose o <> indx B ; :: thesis: (a1 +* (indx B),y) . b₁ in B . b₁

then (a1 +* (indx B),y) . o = a1 . o by FUNCT_7:34;
hence (a1 +* (indx B),y) . o in B . o by A3, A18, A35, A93, CARD_3:18; :: thesis: verum

end;

suppose A94: o = indx B ; :: thesis: (a1 +* (indx B),y) . b₁ in B . b₁

then (a1 +* (indx B),y) . o = y by A4, FUNCT_7:33;
hence (a1 +* (indx B),y) . o in B . o by A45, A70, A94, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then a1 +* (indx B),y in S by A18, A35, A87, CARD_3:18;
then a1 +* (indx B),y in L3 /\ S by A92, XBOOLE_0:def 4;
then 2 c= card (L3 /\ S) by A70, A71, A86, Th2;
then A95: L3 c= S by A2, 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 )
assume A96: e in L ; :: thesis: e in SS
consider f being set such that
A97: f in L3 by XBOOLE_0:def 1;
consider F being Function such that
A98: ( F = f & dom F = I & ( for o being set st o in I holds
F . o in L2 . o ) ) by A75, A97, CARD_3:def 5;
reconsider f = f as ManySortedSet of by A98, PARTFUN1:def 4, RELAT_1:def 18;
A99: dom (f +* (indx B),e) = dom L2 by A75, PARTFUN1:def 4;

now

let o be set ; :: thesis: ( o in dom L2 implies (f +* (indx B),e) . b₁ in L2 . b₁ )
assume A100: o in dom L2 ; :: thesis: (f +* (indx B),e) . b₁ in L2 . b₁

per cases ( o <> indx B or o = indx B ) ;

suppose o <> indx B ; :: thesis: (f +* (indx B),e) . b₁ in L2 . b₁

then (f +* (indx B),e) . o = f . o by FUNCT_7:34;
hence (f +* (indx B),e) . o in L2 . o by A75, A98, A100; :: thesis: verum

end;

suppose A101: o = indx B ; :: thesis: (f +* (indx B),e) . b₁ in L2 . b₁

then (f +* (indx B),e) . o = e by A98, FUNCT_7:33;
hence (f +* (indx B),e) . o in L2 . o by A18, A96, A101, FUNCT_7:33; :: thesis: verum

end;

end;

end;

then f +* (indx B),e in L3 by A99, CARD_3:18;
then (f +* (indx B),e) . (indx B) in B . (indx B) by A18, A35, A95, CARD_3:18;
hence e in SS by A45, A98, FUNCT_7:33; :: thesis: verum

end;

end;

end;

given B being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A102: ( 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: ( not S is trivial & S is strong & S is closed_under_lines )
thus not S is trivial by A102; :: thesis: ( S is strong & S is closed_under_lines )
A103: dom B = I by PARTFUN1:def 4;
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 A104: ( x in S & y in S ) ; :: thesis: x,y are_collinear

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: x,y are_collinear

hence x,y are_collinear by Def1; :: thesis: verum

end;

suppose A105: x <> y ; :: thesis: x,y are_collinear

consider x1 being Function such that
A106: ( x1 = x & dom x1 = dom (Carrier A) & ( for a being set st a in dom (Carrier A) holds
x1 . a in (Carrier A) . a ) ) by CARD_3:def 5;
X: dom (Carrier A) = I by PARTFUN1:def 4;
then reconsider x1 = x1 as ManySortedSet of by A106, PARTFUN1:def 4, RELAT_1:def 18;
consider y1 being Function such that
A107: ( y1 = y & dom y1 = dom (Carrier A) & ( for a being set st a in dom (Carrier A) holds
y1 . a in (Carrier A) . a ) ) by CARD_3:def 5;
reconsider y1 = y1 as ManySortedSet of by X, A107, PARTFUN1:def 4, RELAT_1:def 18;

A108: now

assume A109: x1 . (indx B) = y1 . (indx B) ; :: thesis: contradiction

now

let i be set ; :: thesis: ( i in dom (Carrier A) implies x1 . b₁ = y1 . b₁ )
assume i in dom (Carrier A) ; :: thesis: x1 . b₁ = y1 . b₁

per cases ( i <> indx B or i = indx B ) ;

suppose i <> indx B ; :: thesis: x1 . b₁ = y1 . b₁

hence x1 . i = y1 . i by A102, A104, A106, A107, Th23; :: thesis: verum

end;

suppose i = indx B ; :: thesis: x1 . b₁ = y1 . b₁

hence x1 . i = y1 . i by A109; :: thesis: verum

end;

end;

end;

hence contradiction by A105, A106, A107, FUNCT_1:9; :: thesis: verum

end;

x1 . (indx B) in (Carrier A) . (indx B) by A1, A106;
then reconsider x1i = x1 . (indx B) as Point of (A . (indx B)) by YELLOW_6:9;
y1 . (indx B) in (Carrier A) . (indx B) by A1, A107;
then reconsider y1i = y1 . (indx B) as Point of (A . (indx B)) by YELLOW_6:9;
B c= Carrier A by PBOOLE:def 23;
then B . (indx B) c= (Carrier A) . (indx B) by PBOOLE:def 5;
then reconsider C = B . (indx B) as Subset of (A . (indx B)) by YELLOW_6:9;
A110: x1i in C by A102, A103, A104, A106, CARD_3:18;
A111: y1i in C by A102, A103, A104, A107, CARD_3:18;
C is strong by A102;
then x1i,y1i are_collinear by A110, A111, Def3;
then consider l being Block of (A . (indx B)) such that
A112: {x1i,y1i} c= l by A108, Def1;
A113: dom {x1} = I by PARTFUN1:def 4;
for i being Element of I st i <> indx B holds
( not ({x1} +* (indx B),l) . i is empty & ({x1} +* (indx B),l) . i is trivial )

proof

let i be Element of I; :: thesis: ( i <> indx B implies ( not ({x1} +* (indx B),l) . i is empty & ({x1} +* (indx B),l) . i is trivial ) )
assume i <> indx B ; :: thesis: ( not ({x1} +* (indx B),l) . i is empty & ({x1} +* (indx B),l) . i is trivial )
then ({x1} +* (indx B),l) . i = {x1} . i by FUNCT_7:34
.= {(x1 . i)} by PZFMISC1:def 1 ;
hence ( not ({x1} +* (indx B),l) . i is empty & ({x1} +* (indx B),l) . i is trivial ) ; :: thesis: verum

end;

then A114: {x1} +* (indx B),l is Segre-like by Def20;
{x1} +* (indx B),l c= Carrier A

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or ({x1} +* (indx B),l) . i c= (Carrier A) . i )
assume A115: 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

per cases ( i = indx B or i <> indx B ) ;

suppose A116: i = indx B ; :: thesis: ({x1} +* (indx B),l) . i c= (Carrier A) . i

then ({x1} +* (indx B),l) . i = l by A113, FUNCT_7:33;
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 A116, YELLOW_6:9; :: thesis: verum

end;

suppose i <> indx B ; :: thesis: ({x1} +* (indx B),l) . i c= (Carrier A) . i

then A117: ({x1} +* (indx B),l) . i = {x1} . i by FUNCT_7:34
.= {(x1 . i)} by A115, PZFMISC1:def 1 ;
x1 . i in (Carrier A) . i1 by A1, A106;
then x1 . i in the carrier of (A . i1) by YELLOW_6:9;
then {(x1 . i)} c= the carrier of (A . i1) by ZFMISC_1:37;
hence ({x1} +* (indx B),l) . i c= (Carrier A) . i by A117, YELLOW_6:9; :: thesis: verum

end;

end;

end;

end;

then A118: {x1} +* (indx B),l is ManySortedSubset of Carrier A by PBOOLE:def 23;
({x1} +* (indx B),l) . (indx B) is Block of (A . (indx B)) by A113, FUNCT_7:33;
then reconsider L = product ({x1} +* (indx B),l) as Block of (Segre_Product A) by A114, A118, Def22;
A119: dom x1 = I by PARTFUN1:def 4
.= dom ({x1} +* (indx B),l) by PARTFUN1:def 4 ;
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 A120: a in I by PARTFUN1:def 4;

per cases ( a = indx B or a <> indx B ) ;

suppose A121: a = indx B ; :: thesis: x1 . a in ({x1} +* (indx B),l) . a

then ({x1} +* (indx B),l) . a = l by A113, FUNCT_7:33;
hence x1 . a in ({x1} +* (indx B),l) . a by A112, A121, ZFMISC_1:38; :: thesis: verum

end;

suppose A122: 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 A120, PZFMISC1:def 1;
hence x1 . a in ({x1} +* (indx B),l) . a by A122, FUNCT_7:34; :: thesis: verum

end;

end;

end;

then A123: x1 in L by A119, CARD_3:18;
A124: dom y1 = I by PARTFUN1:def 4
.= dom ({x1} +* (indx B),l) by PARTFUN1:def 4 ;
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 A125: a in I by PARTFUN1:def 4;

per cases ( a = indx B or a <> indx B ) ;

suppose A126: a = indx B ; :: thesis: y1 . a in ({x1} +* (indx B),l) . a

then ({x1} +* (indx B),l) . a = l by A113, FUNCT_7:33;
hence y1 . a in ({x1} +* (indx B),l) . a by A112, A126, ZFMISC_1:38; :: thesis: verum

end;

suppose A127: 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 A125, PZFMISC1:def 1;
then y1 . a in {x1} . a by A102, A104, A106, A107, A127, Th23;
hence y1 . a in ({x1} +* (indx B),l) . a by A127, FUNCT_7:34; :: thesis: verum

end;

end;

end;

then y1 in L by A124, CARD_3:18;
then {x,y} c= L by A106, A107, A123, ZFMISC_1:38;
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 )
assume A128: 2 c= card (l /\ S) ; :: thesis: l c= S
then consider a, b being set such that
A129: ( a in l /\ S & b in l /\ S & a <> b ) by Th2;
reconsider a1 = a, b1 = b as ManySortedSet of by A129, Th14;
consider L being Segre-like ManySortedSubset of Carrier A such that
A130: ( l = product L & ex i being Element of I st L . i is Block of (A . i) ) by Def22;
card (l /\ S) c= card l by CARD_1:27, XBOOLE_1:17;
then 2 c= card l by A128, XBOOLE_1:1;
then reconsider L = L as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A130, Th13;
A131: ( indx B = indx L & ( for i being set st i <> indx B holds
B . i = L . i ) ) by A102, A128, A130, Th26;
A132: dom L = I by PARTFUN1:def 4
.= dom B by PARTFUN1:def 4 ;
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

per cases ( a <> indx B or a = indx B ) ;

suppose a <> indx B ; :: thesis: L . a c= B . a

hence L . a c= B . a by A102, A128, A130, Th26; :: thesis: verum

end;

suppose A133: a = indx B ; :: thesis: L . a c= B . a

consider j being Element of I such that
A134: L . j is Block of (A . j) by A130;
2 c= card (L . j) by A134, 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 A131, A134;
B c= Carrier A by PBOOLE:def 23;
then B . (indx B) c= (Carrier A) . (indx B) by PBOOLE:def 5;
then reconsider C = B . (indx B) as Subset of (A . (indx B)) by YELLOW_6:9;
A135: ( a1 in product B & b1 in product B ) by A102, A129, XBOOLE_0:def 4;

A136: now

assume A137: a1 . (indx B) = b1 . (indx B) ; :: thesis: contradiction
A138: 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

per cases ( o <> indx B or o = indx B ) ;

suppose o <> indx B ; :: thesis: a1 . o = b1 . o

hence a1 . o = b1 . o by A135, Th23; :: thesis: verum

end;

suppose o = indx B ; :: thesis: a1 . o = b1 . o

hence a1 . o = b1 . o by A137; :: thesis: verum

end;

end;

end;

dom a1 = I by PARTFUN1:def 4
.= dom b1 by PARTFUN1:def 4 ;
hence contradiction by A129, A138, FUNCT_1:9; :: thesis: verum

end;

( a1 in product L & b1 in product L ) by A129, A130, XBOOLE_0:def 4;
then A139: ( a1 . (indx B) in L . (indx B) & b1 . (indx B) in L . (indx B) ) by A103, A132, CARD_3:18;
( a1 . (indx B) in B . (indx B) & b1 . (indx B) in B . (indx B) ) by A103, A135, CARD_3:18;
then ( a1 . (indx B) in Li /\ C & b1 . (indx B) in Li /\ C ) by A139, XBOOLE_0:def 4;
then A140: 2 c= card (Li /\ C) by A136, Th2;
C is closed_under_lines by A102;
hence L . a c= B . a by A133, A140, Def2; :: thesis: verum

end;

end;

end;

hence l c= S by A102, A130, A132, CARD_3:38; :: thesis: verum

end;