let PCPP be CollProjectiveSpace; :: thesis: for a1, a2, a3, c3, c1, x being Element of PCPP st not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds
( a1 <> x & a3 <> x )
let a1, a2, a3, c3, c1, x be Element of PCPP; :: thesis: ( not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 implies ( a1 <> x & a3 <> x ) )
assume A1:
( not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 )
; :: thesis: ( a1 <> x & a3 <> x )
A2:
a1 <> x
proof
assume
not
a1 <> x
;
:: thesis: contradiction
then
(
a1,
c3,
c1 is_collinear &
a1,
c3,
a2 is_collinear )
by A1, Th3;
then
a1,
c1,
a2 is_collinear
by A1, Th4;
then
(
a2,
c1,
a1 is_collinear &
a2,
c1,
a3 is_collinear )
by A1, Th3;
then
a2,
a1,
a3 is_collinear
by A1, Th4;
hence
contradiction
by A1, Th3;
:: thesis: verum
end;
a3 <> x
proof
assume
not
a3 <> x
;
:: thesis: contradiction
then
(
a3,
c1,
c3 is_collinear &
a3,
c1,
a2 is_collinear )
by A1, Th3;
then
a3,
a2,
c3 is_collinear
by A1, Th4;
then
(
a2,
c3,
a3 is_collinear &
a2,
c3,
a1 is_collinear )
by A1, Th3;
then
a2,
a1,
a3 is_collinear
by A1, Th4;
hence
contradiction
by A1, Th3;
:: thesis: verum
end;
hence
( a1 <> x & a3 <> x )
by A2; :: thesis: verum