let V be RealLinearSpace; :: thesis: for u, u1, u2, v, v1, v2, w, y 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 u, u1, u2, v, v1, v2, w, y 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 p9 = u, q9 = v, p19 = u1, q19 = v1, p29 = u2, q29 = v2 as Element of the carrier of (AMSpace (V,w,y)) by ANALMETR:19;
reconsider S = AMSpace (V,w,y) as OrtAfSp by A1, ANALMETR:33;
reconsider p = p9, q = q9, p1 = p19, q1 = q19, p2 = p29, q2 = q29 as Element of S ;
A5: ( p2,q2 _|_ p,q or p,q _|_ p2,q2 ) by A3, ANALMETR:21;
( 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:62;
hence ( u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y ) by ANALMETR:21; :: thesis: verum