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