let V be RealLinearSpace; :: thesis: for w, y, u1, v1, u, v, u2, v2 being VECTOR of V st Gen w,y & ( u1,v1 '||' u,v or u,v '||' u1,v1 ) & ( u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y ) & u <> v holds
( u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y )
let w, y, u1, v1, u, v, u2, v2 be VECTOR of V; :: thesis: ( Gen w,y & ( u1,v1 '||' u,v or u,v '||' u1,v1 ) & ( u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y ) & u <> v implies ( u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y ) )
assume that
A1: Gen w,y and
A2: ( u1,v1 '||' u,v or u,v '||' u1,v1 ) and
A3: ( u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y ) and
A4: u <> v ; :: thesis: ( u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y )
reconsider S = AMSpace V,w,y as OrtAfSp by A1, ANALMETR:44;
reconsider p' = u, q' = v, p1' = u1, q1' = v1, p2' = u2, q2' = v2 as Element of the carrier of (AMSpace V,w,y) by ANALMETR:28;
reconsider p = p', q = q', p1 = p1', q1 = q1', p2 = p2', q2 = q2' as Element of S ;
A5: ( p2,q2 _|_ p,q or p,q _|_ p2,q2 ) by A3, ANALMETR:31;
( p1,q1 // p,q or p,q // p1,q1 ) by A2, Th4;
then ( p1,q1 _|_ p2,q2 & p2,q2 _|_ p1,q1 ) by A4, A5, ANALMETR:84;
hence ( u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y ) by ANALMETR:31; :: thesis: verum