let S be OAffinSpace; :: thesis: for x, y, z, t being Element of S st z,x '||' x,t & x <> z holds
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
let x, y, z, t be Element of S; :: thesis: ( z,x '||' x,t & x <> z implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )
assume that
A1: z,x '||' x,t and
A2: x <> z ; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )

A3: now :: thesis: ( z,x // t,x implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )

consider p being Element of S such that
A4: Mid z,x,p and
A5: x <> p by Th13;
A6: z,x // x,p by A4;
then consider q being Element of S such that
A7: y,x // x,q and
A8: y,z // p,q by A2, ANALOAF:def 5;
assume A9: z,x // t,x ; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
then x,p // t,x by A2, A6, ANALOAF:def 5;
then p,x // x,t by Th2;
then consider r being Element of S such that
A10: q,x // x,r and
A11: q,p // t,r by A5, ANALOAF:def 5;

A12: now :: thesis: ( q = p implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )

assume q = p ; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
then A13: x,p // y,x by A7, Th2;
x,p // z,x by A6, Th2;
then z,x // y,x by A5, A13, ANALOAF:def 5;
then y,x // t,x by A2, A9, ANALOAF:def 5;
then A14: y,x '||' x,t ;
y,z // t,t by ANALOAF:def 5;
then y,z '||' t,t ;
hence ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) by A14; :: thesis: verum

end;

A15: now :: thesis: ( q = x implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )

A16: x,z // x,t by A9, Th2;
assume A17: q = x ; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
p,x // x,z by A6, Th2;
then y,z // x,z by A5, A8, A17, Th3;
then y,z // x,t by A2, A16, Th3;
then A18: y,z '||' t,x ;
y,x // x,x by Th4;
then y,x '||' x,x ;
hence ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) by A18; :: thesis: verum

end;

now :: thesis: ( q <> p & q <> x implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )

assume that
A19: q <> p and
A20: q <> x ; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
x,q // r,x by A10, Th2;
then y,x // r,x by A7, A20, Th3;
then A21: y,x '||' x,r ;
p,q // r,t by A11, Th2;
then y,z // r,t by A8, A19, Th3;
then y,z '||' t,r ;
hence ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) by A21; :: thesis: verum

end;

hence ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) by A12, A15; :: thesis: verum

end;

now :: thesis: ( z,x // x,t implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )

assume z,x // x,t ; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
then consider u being Element of S such that
A22: ( y,x // x,u & y,z // t,u ) by A2, ANALOAF:def 5;
( y,x '||' x,u & y,z '||' t,u ) by A22;
hence ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) ; :: thesis: verum

end;

hence ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) by A1, A3; :: thesis: verum