let S be OAffinSpace; :: thesis: for x, y, z being Element of S ex t being Element of S st
( x,z '||' y,t & y <> t )
let x, y, z 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
x,y // z,t and
A1: x,z // y,t and
A2: y <> t by ANALOAF:def 5;
x,z '||' y,t by A1;
hence ex t being Element of S st
( x,z '||' y,t & y <> t ) by A2; :: thesis: verum