let AS be Oriented_Orthogonality_Space; :: thesis: 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; :: thesis: 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; :: thesis: verum