let S be OAffinSpace; :: thesis: for x, y, z being Element of S holds
( x,y '||' z,z & z,z '||' x,y )
let x, y, z be Element of S; :: thesis: ( x,y '||' z,z & z,z '||' x,y )
( x,y // z,z & z,z // x,y ) by Th7;
hence ( x,y '||' z,z & z,z '||' x,y ) by Def4; :: thesis: verum