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