let AS be Oriented_Orthogonality_Space; :: thesis: for u, v, w being Element of ex u1 being Element of st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
let u, v, w be Element of ; :: thesis: ex u1 being Element of st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
consider u1 being Element of 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 st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) ) by A1; :: thesis: verum