hereby :: thesis: ( ( for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear ) implies CS is transitive )
assume A4:
CS is
transitive
;
:: thesis: for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear let p,
q,
r,
r1,
r2 be
Element of
CS;
:: thesis: ( p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear implies r,r1,r2 is_collinear )assume that A5:
p <> q
and A6:
(
p,
q,
r is_collinear &
p,
q,
r1 is_collinear &
p,
q,
r2 is_collinear )
;
:: thesis: r,r1,r2 is_collinear
(
[p,q,r] in the
Collinearity of
CS &
[p,q,r1] in the
Collinearity of
CS &
[p,q,r2] in the
Collinearity of
CS )
by A6, COLLSP:def 2;
then
[r,r1,r2] in the
Collinearity of
CS
by A4, A5, COLLSP:def 4;
hence
r,
r1,
r2 is_collinear
by COLLSP:def 2;
:: thesis: verum
end;
assume A7:
for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear
; :: thesis: CS is transitive
let p, q, r, r1, r2 be Element of CS; :: according to COLLSP:def 4 :: thesis: ( p = q or not [p,q,r] in the Collinearity of CS or not [p,q,r1] in the Collinearity of CS or not [p,q,r2] in the Collinearity of CS or [r,r1,r2] in the Collinearity of CS )
assume that
A8:
p <> q
and
A9:
( [p,q,r] in the Collinearity of CS & [p,q,r1] in the Collinearity of CS & [p,q,r2] in the Collinearity of CS )
; :: thesis: [r,r1,r2] in the Collinearity of CS
( p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear )
by A9, COLLSP:def 2;
then
r,r1,r2 is_collinear
by A7, A8;
hence
[r,r1,r2] in the Collinearity of CS
by COLLSP:def 2; :: thesis: verum