let S be OAffinSpace; :: thesis: for x, y, z, t being Element of S st x,y,z is_collinear & x,y,t is_collinear holds
x,y '||' z,t
let x, y, z, t be Element of S; :: thesis: ( x,y,z is_collinear & x,y,t is_collinear implies x,y '||' z,t )
assume A1:
( x,y,z is_collinear & x,y,t is_collinear )
; :: thesis: x,y '||' z,t
now assume A2:
x <> y
;
:: thesis: x,y '||' z,tnow A3:
(
x,
y '||' x,
z &
x,
y '||' x,
t )
by A1, Def5;
then
x,
z '||' x,
t
by A2, Th28;
then
z,
x '||' z,
t
by Th26;
then
x,
z '||' z,
t
by Th27;
hence
x,
y '||' z,
t
by A3, Th28;
:: thesis: verum end; hence
x,
y '||' z,
t
;
:: thesis: verum end;
hence
x,y '||' z,t
by Th25; :: thesis: verum