let CPS be proper CollSp; for a, b, c being POINT of (IncProjSp_of CPS)
for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
let a, b, c be POINT of (IncProjSp_of CPS); for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
let a9, b9, c9 be Point of CPS; ( a = a9 & b = b9 & c = c9 implies ( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) ) )
assume that
A1:
a = a9
and
A2:
b = b9
and
A3:
c = c9
; ( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
hereby ( ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) implies a9,b9,c9 are_collinear )
assume A4:
a9,
b9,
c9 are_collinear
;
ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )A5:
now ( a9 <> b9 implies ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )set X =
Line (
a9,
b9);
assume
a9 <> b9
;
ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )then reconsider P9 =
Line (
a9,
b9) as
LINE of
CPS by COLLSP:def 7;
reconsider P =
P9 as
LINE of
(IncProjSp_of CPS) by Th1;
a9 in Line (
a9,
b9)
by COLLSP:10;
then A6:
a on P
by A1, Th5;
b9 in Line (
a9,
b9)
by COLLSP:10;
then A7:
b on P
by A2, Th5;
c9 in Line (
a9,
b9)
by A4, COLLSP:11;
then
c on P
by A3, Th5;
hence
ex
P being
LINE of
(IncProjSp_of CPS) st
(
a on P &
b on P &
c on P )
by A6, A7;
verum end; hence
ex
P being
LINE of
(IncProjSp_of CPS) st
(
a on P &
b on P &
c on P )
by A5;
verum
end;
given P being LINE of (IncProjSp_of CPS) such that A9:
( a on P & b on P )
and
A10:
c on P
; a9,b9,c9 are_collinear
reconsider P9 = P as LINE of CPS by Th1;
A11:
c9 in P9
by A3, A10, Th5;
( a9 in P9 & b9 in P9 )
by A1, A2, A9, Th5;
hence
a9,b9,c9 are_collinear
by A11, COLLSP:16; verum