let L be Z_Lattice; :: thesis: for v, u being Vector of L st v,u are_orthogonal holds
( v, - u are_orthogonal & - v,u are_orthogonal & - v, - u are_orthogonal )
let v, u be Vector of L; :: thesis: ( v,u are_orthogonal implies ( v, - u are_orthogonal & - v,u are_orthogonal & - v, - u are_orthogonal ) )
assume A1: v,u are_orthogonal ; :: thesis: ( v, - u are_orthogonal & - v,u are_orthogonal & - v, - u are_orthogonal )
<;v,(- u);> = - <;v,u;> by ThSc1
.= 0 by A1 ;
hence v, - u are_orthogonal ; :: thesis: ( - v,u are_orthogonal & - v, - u are_orthogonal )
A2: <;(- v),u;> = - <;v,u;> by ThSc1
.= 0 by A1 ;
hence - v,u are_orthogonal ; :: thesis: - v, - u are_orthogonal
<;(- v),(- u);> = - <;(- v),u;> by ThSc1
.= 0 by A2 ;
hence - v, - u are_orthogonal ; :: thesis: verum