let S be OAffinSpace; :: thesis: for x, z, y being Element of S ex t being Element of S st
( x,z '||' y,t & y <> t )
let x, z, y be Element of S; :: thesis: ex t being Element of S st
( x,z '||' y,t & y <> t )
consider t being Element of S such that
A1: ( x,y // z,t & x,z // y,t & y <> t ) by ANALOAF:def 5;
x,z '||' y,t by A1, Def4;
hence ex t being Element of S st
( x,z '||' y,t & y <> t ) by A1; :: thesis: verum