let V be RealLinearSpace; :: thesis: for u, u1, v, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
let u, u1, v, v1, x, y be VECTOR of V; :: thesis: for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
let p, q, r, s be Element of (CMSpace (V,x,y)); :: thesis: ( u = p & v = q & u1 = r & v1 = s implies ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) )
assume that
A1: u = p and
A2: v = q and
A3: u1 = r and
A4: v1 = s ; :: thesis: ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
A5: ( p,q _|_ r,s implies u,v,u1,v1 are_COrtm_wrt x,y )

proof

assume p,q _|_ r,s ; :: thesis: u,v,u1,v1 are_COrtm_wrt x,y
then [[p,q],[r,s]] in the orthogonality of (CMSpace (V,x,y)) by ANALMETR:def 5;
then consider u19, u29, v19, v29 being VECTOR of V such that
A6: [u,v] = [u19,u29] and
A7: [u1,v1] = [v19,v29] and
A8: u19,u29,v19,v29 are_COrtm_wrt x,y by A1, A2, A3, A4, Def6;
A9: u = u19 by A6, XTUPLE_0:1;
A10: v = u29 by A6, XTUPLE_0:1;
u1 = v19 by A7, XTUPLE_0:1;
hence u,v,u1,v1 are_COrtm_wrt x,y by A7, A8, A9, A10, XTUPLE_0:1; :: thesis: verum

end;

( u,v,u1,v1 are_COrtm_wrt x,y implies p,q _|_ r,s )

proof

assume u,v,u1,v1 are_COrtm_wrt x,y ; :: thesis: p,q _|_ r,s
then [[u,v],[u1,v1]] in the orthogonality of OrtStr(# the carrier of V,(CORTM (V,x,y)) #) by Def6;
hence p,q _|_ r,s by A1, A2, A3, A4, ANALMETR:def 5; :: thesis: verum

end;

hence ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) by A5; :: thesis: verum