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 )

A1: now

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

end;

A2: now

A3: now

assume x,z // z,y ; :: thesis: ( x,y '||' x,z implies 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 ( x,y '||' x,z implies y,x '||' y,z ) by Def4; :: thesis: verum

end;

A4: now

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

end;

assume x,y // x,z ; :: thesis: ( x,y '||' x,z implies y,x '||' y,z )
hence ( x,y '||' x,z implies y,x '||' y,z ) by A4, A3, ANALOAF:def 5; :: thesis: verum

end;

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