let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st B1 misses B2 holds
( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds
( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 misses B2 implies ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) ) )

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A1: B1 = product L1 and
L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;
assume A2: B1 misses B2 ; :: thesis: ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )

thus ( B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) ) :: thesis: ( ( for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) ) implies B1 '||' B2 )
proof
assume A3: B1 '||' B2 ; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) )

consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A4: B2 = product L2 and
A5: L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A6: B1 = product L1 and
A7: L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & B2 = product b2 implies ( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )

assume that
A8: B1 = product b1 and
A9: B2 = product b2 ; :: thesis: ( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) )

A10: b1 = L1 by ;
thus A11: indx b1 = indx b2 :: thesis: ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) )
proof
assume indx b1 <> indx b2 ; :: thesis: contradiction
then b2 . (indx b1) is 1 -element by PENCIL_1:12;
then consider c2 being object such that
A12: b2 . (indx b1) = {c2} by ZFMISC_1:131;
set bl = the Block of (A . (indx b1));
consider p0 being object such that
A13: p0 in B1 by ;
reconsider p0 = p0 as Point of () by A13;
reconsider p = p0 as Element of Carrier A by Th6;
the Block of (A . (indx b1)) in the topology of (A . (indx b1)) ;
then ( 2 c= card the Block of (A . (indx b1)) & card the Block of (A . (indx b1)) c= card the carrier of (A . (indx b1)) ) by ;
then consider a being object such that
A14: a in the carrier of (A . (indx b1)) and
A15: a <> c2 by ;
reconsider a = a as Point of (A . (indx b1)) by A14;
reconsider x = p +* ((indx b1),a) as Point of () by PENCIL_1:25;
reconsider x1 = x as Element of Carrier A by Th6;
A16: dom x1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2 ;
now :: thesis: for i being object st i in dom x1 holds
x1 . i in b1 . i
let i be object ; :: thesis: ( i in dom x1 implies x1 . b1 in b1 . b1 )
assume A17: i in dom x1 ; :: thesis: x1 . b1 in b1 . b1
then i in I ;
then A18: i in dom p by PARTFUN1:def 2;
per cases ( i = indx b1 or i <> indx b1 ) ;
suppose A19: i = indx b1 ; :: thesis: x1 . b1 in b1 . b1
then x1 . i = a by ;
hence x1 . i in b1 . i by A7, A10, A19; :: thesis: verum
end;
suppose i <> indx b1 ; :: thesis: x1 . b1 in b1 . b1
then A20: x1 . i = p . i by FUNCT_7:32;
ex f being Function st
( f = p & dom f = dom b1 & ( for a being object st a in dom b1 holds
f . a in b1 . a ) ) by ;
hence x1 . i in b1 . i by ; :: thesis: verum
end;
end;
end;
then A21: x in B1 by ;
then consider y being Point of () such that
A22: y in B2 and
A23: x,y are_collinear by A3;
reconsider y1 = y as Element of Carrier A by Th6;
per cases ( y = x or y <> x ) ;
suppose y = x ; :: thesis: contradiction
end;
suppose y <> x ; :: thesis: contradiction
then consider i0 being Element of I such that
for a, b being Point of (A . i0) st a = x1 . i0 & b = y1 . i0 holds
( a <> b & a,b are_collinear ) and
A24: for j being Element of I st j <> i0 holds
x1 . j = y1 . j by ;
A25: dom y1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2 ;
now :: thesis: for i being object st i in dom y1 holds
y1 . i in b1 . i
let i be object ; :: thesis: ( i in dom y1 implies y1 . b1 in b1 . b1 )
assume A26: i in dom y1 ; :: thesis: y1 . b1 in b1 . b1
then reconsider i5 = i as Element of I ;
per cases ( i = indx b1 or i <> indx b1 ) ;
suppose A27: i = indx b1 ; :: thesis: y1 . b1 in b1 . b1
reconsider i1 = i as Element of I by A26;
y1 . i1 is Element of () . i1 by PBOOLE:def 14;
then y1 . i1 is Element of [#] (A . i1) by Th7;
hence y1 . i in b1 . i by A7, A10, A27; :: thesis: verum
end;
suppose A28: i <> indx b1 ; :: thesis: y1 . b1 in b1 . b1
( ex g being Function st
( g = y1 & dom g = dom b2 & ( for a being object st a in dom b2 holds
g . a in b2 . a ) ) & dom b2 = I ) by ;
then y1 . (indx b1) in b2 . (indx b1) ;
then A29: y1 . (indx b1) = c2 by ;
dom p = I by PARTFUN1:def 2;
then x1 . (indx b1) = a by FUNCT_7:31;
then i0 = indx b1 by ;
then A30: y1 . i5 = x1 . i5 by ;
A31: x1 . i = p . i by ;
ex f being Function st
( f = p & dom f = dom b1 & ( for a being object st a in dom b1 holds
f . a in b1 . a ) ) by ;
hence y1 . i in b1 . i by A25, A26, A30, A31; :: thesis: verum
end;
end;
end;
then y in B1 by ;
then y in B1 /\ B2 by ;
hence contradiction by A2; :: thesis: verum
end;
end;
end;
A32: b2 = L2 by ;
thus ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) :: thesis: verum
proof
consider x being object such that
A33: x in B1 by ;
reconsider x = x as Point of () by A33;
consider y being Point of () such that
A34: y in B2 and
A35: x,y are_collinear by ;
reconsider y1 = y as Element of Carrier A by Th6;
reconsider x1 = x as Element of Carrier A by Th6;
x <> y by ;
then consider r being Element of I such that
A36: for a, b being Point of (A . r) st a = x1 . r & b = y1 . r holds
( a <> b & a,b are_collinear ) and
A37: for j being Element of I st j <> r holds
x1 . j = y1 . j by ;
take r ; :: thesis: ( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) )

now :: thesis: not r = indx b1
assume A38: r = indx b1 ; :: thesis: contradiction
A39: now :: thesis: for o being object st o in dom b1 holds
y1 . o in b1 . o
let o be object ; :: thesis: ( o in dom b1 implies y1 . b1 in b1 . b1 )
assume A40: o in dom b1 ; :: thesis: y1 . b1 in b1 . b1
then reconsider o1 = o as Element of I ;
per cases ( o1 = r or o1 <> r ) ;
suppose A41: o1 = r ; :: thesis: y1 . b1 in b1 . b1
y1 . o1 is Element of () . o1 by PBOOLE:def 14;
then y1 . o1 is Element of [#] (A . o1) by Th7;
hence y1 . o in b1 . o by A7, A10, A38, A41; :: thesis: verum
end;
suppose A42: o1 <> r ; :: thesis: y1 . b1 in b1 . b1
then b1 . o1 is 1 -element by ;
then consider c being object such that
A43: b1 . o1 = {c} by ZFMISC_1:131;
x1 . o1 in b1 . o1 by ;
then c = x1 . o1 by
.= y1 . o1 by ;
hence y1 . o in b1 . o by ; :: thesis: verum
end;
end;
end;
dom y1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2 ;
then y1 in B1 by ;
then B1 /\ B2 <> {} by ;
hence contradiction by A2; :: thesis: verum
end;
hence r <> indx b1 ; :: thesis: ( ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) )

thus for i being Element of I st i <> r holds
b1 . i = b2 . i :: thesis: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear
proof
let i be Element of I; :: thesis: ( i <> r implies b1 . i = b2 . i )
assume A44: i <> r ; :: thesis: b1 . i = b2 . i
per cases ( i = indx b1 or i <> indx b1 ) ;
suppose i = indx b1 ; :: thesis: b1 . i = b2 . i
hence b1 . i = b2 . i by A7, A5, A10, A32, A11; :: thesis: verum
end;
suppose A45: i <> indx b1 ; :: thesis: b1 . i = b2 . i
then b2 . i is 1 -element by ;
then A46: ex d being object st b2 . i = {d} by ZFMISC_1:131;
dom b2 = I by PARTFUN1:def 2;
then A47: y1 . i in b2 . i by ;
b1 . i is 1 -element by ;
then consider c being object such that
A48: b1 . i = {c} by ZFMISC_1:131;
dom b1 = I by PARTFUN1:def 2;
then x1 . i in b1 . i by ;
then c = x1 . i by
.= y1 . i by ;
hence b1 . i = b2 . i by ; :: thesis: verum
end;
end;
end;
let c1, c2 be Point of (A . r); :: thesis: ( b1 . r = {c1} & b2 . r = {c2} implies c1,c2 are_collinear )
assume that
A49: b1 . r = {c1} and
A50: b2 . r = {c2} ; :: thesis: c1,c2 are_collinear
dom L2 = I by PARTFUN1:def 2;
then y1 . r in b2 . r by ;
then A51: c2 = y1 . r by ;
dom L1 = I by PARTFUN1:def 2;
then x1 . r in b1 . r by ;
then c1 = x1 . r by ;
hence c1,c2 are_collinear by ; :: thesis: verum
end;
end;
consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A52: B2 = product L2 and
L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;
assume A53: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) ; :: thesis: B1 '||' B2
then consider r being Element of I such that
A54: r <> indx L1 and
A55: for i being Element of I st i <> r holds
L1 . i = L2 . i and
A56: for c1, c2 being Point of (A . r) st L1 . r = {c1} & L2 . r = {c2} holds
c1,c2 are_collinear by ;
indx L1 = indx L2 by A53, A1, A52;
then L2 . r is 1 -element by ;
then consider c2 being object such that
A57: L2 . r = {c2} by ZFMISC_1:131;
L2 c= Carrier A by PBOOLE:def 18;
then L2 . r c= () . r ;
then {c2} c= [#] (A . r) by ;
then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:31;
L1 . r is 1 -element by ;
then consider c1 being object such that
A58: L1 . r = {c1} by ZFMISC_1:131;
L1 c= Carrier A by PBOOLE:def 18;
then L1 . r c= () . r ;
then {c1} c= [#] (A . r) by ;
then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;
A59: now :: thesis: not c1 = c2
assume A60: c1 = c2 ; :: thesis: contradiction
A61: now :: thesis: for s being object st s in dom L1 holds
L1 . s = L2 . s
let s be object ; :: thesis: ( s in dom L1 implies L1 . b1 = L2 . b1 )
assume s in dom L1 ; :: thesis: L1 . b1 = L2 . b1
then reconsider s1 = s as Element of I ;
per cases ( s1 = r or s1 <> r ) ;
suppose s1 = r ; :: thesis: L1 . b1 = L2 . b1
hence L1 . s = L2 . s by ; :: thesis: verum
end;
suppose s1 <> r ; :: thesis: L1 . b1 = L2 . b1
hence L1 . s = L2 . s by A55; :: thesis: verum
end;
end;
end;
dom L1 = I by PARTFUN1:def 2
.= dom L2 by PARTFUN1:def 2 ;
then L1 = L2 by A61;
then B1 /\ B1 = {} by A2, A1, A52;
hence contradiction by A1; :: thesis: verum
end;
c1,c2 are_collinear by ;
then consider bb being Block of (A . r) such that
A62: {c1,c2} c= bb by ;
let x be Point of (); :: according to PENCIL_3:def 2 :: thesis: ( x in B1 implies ex y being Point of () st
( y in B2 & x,y are_collinear ) )

reconsider x1 = x as Element of Carrier A by Th6;
reconsider y = x1 +* (r,c2) as Point of () by PENCIL_1:25;
reconsider y1 = y as ManySortedSet of I ;
assume x in B1 ; :: thesis: ex y being Point of () st
( y in B2 & x,y are_collinear )

then A63: ex x2 being Function st
( x2 = x & dom x2 = dom L1 & ( for o being object st o in dom L1 holds
x2 . o in L1 . o ) ) by ;
A64: now :: thesis: for a being object st a in dom L2 holds
y1 . a in L2 . a
let a be object ; :: thesis: ( a in dom L2 implies y1 . b1 in L2 . b1 )
assume a in dom L2 ; :: thesis: y1 . b1 in L2 . b1
then reconsider a1 = a as Element of I ;
per cases ( a1 = r or a1 <> r ) ;
suppose A65: a1 = r ; :: thesis: y1 . b1 in L2 . b1
dom x1 = I by PARTFUN1:def 2;
then y1 . a = c2 by ;
hence y1 . a in L2 . a by ; :: thesis: verum
end;
suppose A66: a1 <> r ; :: thesis: y1 . b1 in L2 . b1
then ( dom x1 = I & y1 . a1 = x1 . a1 ) by ;
then y1 . a1 in L1 . a1 by A63;
hence y1 . a in L2 . a by ; :: thesis: verum
end;
end;
end;
take y ; :: thesis: ( y in B2 & x,y are_collinear )
dom y1 = I by PARTFUN1:def 2
.= dom L2 by PARTFUN1:def 2 ;
hence y in B2 by ; :: thesis:
reconsider B = product ({x1} +* (r,bb)) as Block of () by Th16;
A67: now :: thesis: for s being object st s in dom y1 holds
y1 . s in ({x1} +* (r,bb)) . s
let s be object ; :: thesis: ( s in dom y1 implies y1 . b1 in ({x1} +* (r,bb)) . b1 )
assume s in dom y1 ; :: thesis: y1 . b1 in ({x1} +* (r,bb)) . b1
then A68: s in I ;
then A69: ( s in dom {x1} & s in dom x1 ) by PARTFUN1:def 2;
per cases ( s = r or s <> r ) ;
suppose s = r ; :: thesis: y1 . b1 in ({x1} +* (r,bb)) . b1
then ( y1 . s = c2 & bb = ({x1} +* (r,bb)) . s ) by ;
hence y1 . s in ({x1} +* (r,bb)) . s by ; :: thesis: verum
end;
suppose A70: s <> r ; :: thesis: y1 . b1 in ({x1} +* (r,bb)) . b1
then {x1} . s = ({x1} +* (r,bb)) . s by FUNCT_7:32;
then A71: {(x1 . s)} = ({x1} +* (r,bb)) . s by ;
y1 . s = x1 . s by ;
hence y1 . s in ({x1} +* (r,bb)) . s by ; :: thesis: verum
end;
end;
end;
dom y1 = I by PARTFUN1:def 2
.= dom ({x1} +* (r,bb)) by PARTFUN1:def 2 ;
then A72: y in B by ;
A73: now :: thesis: for s being object st s in dom x1 holds
x1 . s in ({x1} +* (r,bb)) . s
let s be object ; :: thesis: ( s in dom x1 implies x1 . b1 in ({x1} +* (r,bb)) . b1 )
assume A74: s in dom x1 ; :: thesis: x1 . b1 in ({x1} +* (r,bb)) . b1
then A75: s in I ;
then A76: s in dom {x1} by PARTFUN1:def 2;
per cases ( s = r or s <> r ) ;
suppose A77: s = r ; :: thesis: x1 . b1 in ({x1} +* (r,bb)) . b1
x1 . s in L1 . s by ;
then A78: x1 . s = c1 by ;
bb = ({x1} +* (r,bb)) . s by ;
hence x1 . s in ({x1} +* (r,bb)) . s by ; :: thesis: verum
end;
suppose s <> r ; :: thesis: x1 . b1 in ({x1} +* (r,bb)) . b1
then {x1} . s = ({x1} +* (r,bb)) . s by FUNCT_7:32;
then {(x1 . s)} = ({x1} +* (r,bb)) . s by ;
hence x1 . s in ({x1} +* (r,bb)) . s by TARSKI:def 1; :: thesis: verum
end;
end;
end;
dom x1 = I by PARTFUN1:def 2
.= dom ({x1} +* (r,bb)) by PARTFUN1:def 2 ;
then x in B by ;
then {x,y} c= B by ;
hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum