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 '||' B2 holds
for f being Collineation of ()
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2

let A be PLS-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st B1 '||' B2 holds
for f being Collineation of ()
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 '||' B2 implies for f being Collineation of ()
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2 )

assume A1: B1 '||' B2 ; :: thesis: for f being Collineation of ()
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2

let f be Collineation of (); :: thesis: for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2

let C1, C2 be Segre-Coset of A; :: thesis: ( C1 = f .: B1 & C2 = f .: B2 implies C1 '||' C2 )
assume that
A2: C1 = f .: B1 and
A3: C2 = f .: B2 ; :: thesis: C1 '||' C2
let x be Point of (); :: according to PENCIL_3:def 2 :: thesis: ( x in C1 implies ex y being Point of () st
( y in C2 & x,y are_collinear ) )

assume x in C1 ; :: thesis: ex y being Point of () st
( y in C2 & x,y are_collinear )

then consider a being object such that
A4: a in dom f and
A5: a in B1 and
A6: x = f . a by ;
reconsider a = a as Point of () by A4;
consider b being Point of () such that
A7: b in B2 and
A8: a,b are_collinear by A1, A5;
take y = f . b; :: thesis: ( y in C2 & x,y are_collinear )
A9: dom f = the carrier of () by FUNCT_2:def 1;
hence y in C2 by ; :: thesis:
per cases ( a = b or a <> b ) ;
suppose a = b ; :: thesis:
end;
suppose a <> b ; :: thesis:
then consider l being Block of () such that
A10: {a,b} c= l by ;
reconsider k = f .: l as Block of () ;
b in l by ;
then A11: y in k by ;
a in l by ;
then x in k by ;
then {x,y} c= k by ;
hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum
end;
end;