let S be OAffinSpace; :: thesis: for x, y, z, t, u, w being Element of S st x <> y & x,y '||' z,t & x,y '||' u,w holds
z,t '||' u,w
let x, y, z, t, u, w be Element of S; :: thesis: ( x <> y & x,y '||' z,t & x,y '||' u,w implies z,t '||' u,w )
assume that
A1: x <> y and
A2: x,y '||' z,t and
A3: x,y '||' u,w ; :: thesis: z,t '||' u,w
A4: ( x,y // u,w or x,y // w,u ) by A3;

A5: now :: thesis: ( x,y // t,z implies z,t '||' u,w )

assume x,y // t,z ; :: thesis: z,t '||' u,w
then ( t,z // u,w or t,z // w,u ) by A1, A4, ANALOAF:def 5;
then ( z,t // w,u or z,t // u,w ) by ANALOAF:def 5;
hence z,t '||' u,w ; :: thesis: verum

end;

( x,y // z,t implies z,t '||' u,w ) by A1, A4, ANALOAF:def 5;
hence z,t '||' u,w by A2, A5; :: thesis: verum