let S be OAffinSpace; :: thesis: not for x, y, z being Element of S holds x,y '||' x,z
consider x, y, z, t being Element of S such that
A1: not x,y // z,t and
A2: not x,y // t,z by ANALOAF:def 5;
A3: x <> y by A1, Th4;

now :: thesis: ( x,y '||' x,z implies not x,y '||' x,t )

assume A4: x,y '||' x,z ; :: thesis: not x,y '||' x,t
thus not x,y '||' x,t :: thesis: verum

proof

assume A5: x,y '||' x,t ; :: thesis: contradiction
then x,z '||' x,t by A3, A4, Th23;
then z,x '||' z,t by Th21;
then x,z '||' z,t by Th22;
then ( x,y '||' z,t or x = z ) by A4, Th23;
hence contradiction by A1, A2, A5; :: thesis: verum

end;

end;

hence not for x, y, z being Element of S holds x,y '||' x,z ; :: thesis: verum