let CPS be proper CollSp; :: thesis: for a, b, c being POINT of (IncProjSp_of CPS)
for a', b', c' being Point of CPS st a = a' & b = b' & c = c' holds
( a',b',c' is_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); :: thesis: for a', b', c' being Point of CPS st a = a' & b = b' & c = c' holds
( a',b',c' is_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 CPS; :: thesis: ( a = a' & b = b' & c = c' implies ( a',b',c' is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) ) )
assume A1:
( a = a' & b = b' & c = c' )
; :: thesis: ( a',b',c' is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
hereby :: thesis: ( ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) implies a',b',c' is_collinear )
assume A2:
a',
b',
c' is_collinear
;
:: thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )A3:
now assume A4:
a' <> b'
;
:: thesis: ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P )set X =
Line a',
b';
A5:
(
a' in Line a',
b' &
b' in Line a',
b' &
c' in Line a',
b' )
by A2, COLLSP:16, COLLSP:17;
reconsider P' =
Line a',
b' as
LINE of
CPS by A4, COLLSP:def 7;
reconsider P =
P' as
LINE of
(IncProjSp_of CPS) by Th2;
(
a on P &
b on P &
c on P )
by A1, A5, Th9;
hence
ex
P being
LINE of
(IncProjSp_of CPS) st
(
a on P &
b on P &
c on P )
;
:: thesis: verum end; hence
ex
P being
LINE of
(IncProjSp_of CPS) st
(
a on P &
b on P &
c on P )
by A3;
:: thesis: verum
end;
given P being LINE of (IncProjSp_of CPS) such that A7:
( a on P & b on P & c on P )
; :: thesis: a',b',c' is_collinear
reconsider P' = P as LINE of CPS by Th2;
( a' in P' & b' in P' & c' in P' )
by A1, A7, Th9;
hence
a',b',c' is_collinear
by COLLSP:25; :: thesis: verum