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 :: thesis: ( x,y // z,x & x,y '||' x,z implies y,x '||' y,z )

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

end;

A2: now :: thesis: ( x,y // x,z & x,y '||' x,z implies y,x '||' y,z )

A3: now :: thesis: ( x,z // z,y & x,y '||' x,z implies y,x '||' y,z )

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

end;

A4: ( x,y // y,z & x,y '||' x,z implies y,x '||' y,z ) by ANALOAF:def 5;
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; :: thesis: verum