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