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, Def4;

A5: now

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 by Def4; :: thesis: verum

end;

now

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

end;

hence z,t '||' u,w by A2, A5, Def4; :: thesis: verum