let S be OAffinSpace; :: thesis: for x, y, z being Element of S st x,y '||' x,z holds
y,x '||' y,z
let x, y, z be Element of S; :: thesis: ( x,y '||' x,z implies y,x '||' y,z )
assume A1: x,y '||' x,z ; :: thesis: y,x '||' y,z

A2: now

assume A3: x,y // x,z ; :: thesis: y,x '||' y,z

A4: now

assume x,y // y,z ; :: thesis: y,x '||' y,z
then y,x // z,y by ANALOAF:def 5;
hence y,x '||' y,z by Def4; :: thesis: verum

end;

now

assume x,z // z,y ; :: thesis: y,x '||' y,z
then y,z // z,x by Th5;
then y,z // y,x by ANALOAF:def 5;
then y,x // y,z by Th5;
hence y,x '||' y,z by Def4; :: thesis: verum

end;

hence y,x '||' y,z by A3, A4, ANALOAF:def 5; :: thesis: verum

end;

now

assume x,y // z,x ; :: thesis: y,x '||' y,z
then y,x // x,z by ANALOAF:def 5;
then y,x // y,z by ANALOAF:def 5;
hence y,x '||' y,z by Def4; :: thesis: verum

end;

hence y,x '||' y,z by A1, A2, Def4; :: thesis: verum