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