let FdSp be FanodesSp; for a, b, p, q, o being Element of FdSp st o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear holds
a,b '||' p,q
let a, b, p, q, o be Element of FdSp; ( o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear implies a,b '||' p,q )
assume that
A1:
o <> a
and
A2:
o <> b
and
A3:
o,a,b are_collinear
and
A4:
o,a,p are_collinear
and
A5:
o,b,q are_collinear
; a,b '||' p,q
A6:
now ( o <> p implies a,b '||' p,q )A7:
o,
a '||' o,
b
by A3;
o,
a '||' o,
p
by A4;
then A8:
o,
b '||' o,
p
by A1, A7, PARSP_1:def 12;
o,
b '||' o,
q
by A5;
then
o,
p '||' o,
q
by A2, A8, PARSP_1:def 12;
then A9:
o,
p '||' p,
q
by PARSP_1:24;
o,
b '||' a,
b
by A7, PARSP_1:24;
then A10:
a,
b '||' o,
p
by A2, A8, PARSP_1:def 12;
assume
o <> p
;
a,b '||' p,qhence
a,
b '||' p,
q
by A10, A9, PARSP_1:26;
verum end;
now ( o = p implies a,b '||' p,q )assume A11:
o = p
;
a,b '||' p,qthen
p,
a '||' p,
b
by A3;
then A12:
a,
b '||' p,
b
by PARSP_1:24;
p,
b '||' p,
q
by A5, A11;
hence
a,
b '||' p,
q
by A2, A11, A12, PARSP_1:26;
verum end;
hence
a,b '||' p,q
by A6; verum