let V be RealLinearSpace; :: thesis: for u, u1, v, v1, x, y being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y & not u = v holds
u1 = v1
let u, u1, v, v1, x, y be VECTOR of V; :: thesis: ( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y & not u = v implies u1 = v1 )
assume A1: Gen x,y ; :: thesis: ( not u,v,u1,v1 are_COrte_wrt x,y or not u,v,v1,u1 are_COrte_wrt x,y or u = v or u1 = v1 )
assume that
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,v1,u1 are_COrte_wrt x,y ; :: thesis: ( u = v or u1 = v1 )
assume that
A4: u <> v and
A5: u1 <> v1 ; :: thesis: contradiction
A6: Orte (x,y,u), Orte (x,y,v) // u1,v1 by A2;
A7: Orte (x,y,u), Orte (x,y,v) // v1,u1 by A3;
Orte (x,y,u) <> Orte (x,y,v) by A1, A4, Th13;
hence contradiction by A5, A6, A7, ANALOAF:10, ANALOAF:11; :: thesis: verum