let AS be Oriented_Orthogonality_Space; for u, v, w being Element of AS ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
let u, v, w be Element of AS; ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
consider u1 being Element of AS such that
A1:
u <> u1
and
A2:
u,u1 '//' v,w
by Def1;
( v,w '//' u,u1 or v,w '//' u1,u )
by A2, Def1;
hence
ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
by A1; verum