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

( 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