let S be OAffinPlane; :: thesis: for x, y, z, t being Element of S st not x,y '||' z,t holds
ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u )
let x, y, z, t be Element of S; :: thesis: ( not x,y '||' z,t implies ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u ) )
assume not x,y '||' z,t ; :: thesis: ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u )
then ( not x,y // z,t & not x,y // t,z ) ;
then consider u being Element of S such that
A1: ( ( x,y // x,u or x,y // u,x ) & ( z,t // z,u or z,t // u,z ) ) by ANALOAF:def 6;
( x,y '||' x,u & z,t '||' z,u ) by A1;
hence ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u ) ; :: thesis: verum