let V be RealLinearSpace; :: thesis: for u, v, u1, v1, x, y being VECTOR of
for p, q, r, s being Element of st u = p & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
let u, v, u1, v1, x, y be VECTOR of ; :: thesis: for p, q, r, s being Element of st u = p & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
let p, q, r, s be Element of ; :: thesis: ( u = p & v = q & u1 = r & v1 = s implies ( p,q // r,s iff u,v,u1,v1 are_COrte_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_COrte_wrt x,y )
A5: ( p,q // r,s implies u,v,u1,v1 are_COrte_wrt x,y )

proof

assume p,q // r,s ; :: thesis: u,v,u1,v1 are_COrte_wrt x,y
then [[p,q],[r,s]] in the CONGR of (CESpace V,x,y) by ANALOAF:def 2;
then consider u1', u2', v1', v2' being VECTOR of such that
A6: [u,v] = [u1',u2'] and
A7: [u1,v1] = [v1',v2'] and
A8: u1',u2',v1',v2' are_COrte_wrt x,y by A1, A2, A3, A4, Def5;
A9: u = u1' by A6, ZFMISC_1:33;
A10: v = u2' by A6, ZFMISC_1:33;
u1 = v1' by A7, ZFMISC_1:33;
hence u,v,u1,v1 are_COrte_wrt x,y by A7, A8, A9, A10, ZFMISC_1:33; :: thesis: verum

end;

( u,v,u1,v1 are_COrte_wrt x,y implies p,q // r,s )

proof

assume u,v,u1,v1 are_COrte_wrt x,y ; :: thesis: p,q // r,s
then [[u,v],[u1,v1]] in the CONGR of AffinStruct(# the carrier of V,(CORTE V,x,y) #) by Def5;
hence p,q // r,s by A1, A2, A3, A4, ANALOAF:def 2; :: thesis: verum

end;

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