let AS be AffinSpace; for a, b, a9, b9, q being Element of AS
for M, N being Subset of AS st q in M & q in N & a in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & q = a9 holds
q = b9
let a, b, a9, b9, q be Element of AS; for M, N being Subset of AS st q in M & q in N & a in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & q = a9 holds
q = b9
let M, N be Subset of AS; ( q in M & q in N & a in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & q = a9 implies q = b9 )
assume that
A1:
q in M
and
A2:
q in N
and
A3:
a in M
and
A4:
b in N
and
A5:
b9 in N
and
A6:
q <> a
and
A7:
( q <> b & M <> N )
and
A8:
( a,b // a9,b9 or b,a // b9,a9 )
and
A9:
M is being_line
and
A10:
N is being_line
and
A11:
q = a9
; q = b9
A12:
not LIN q,a,b
proof
assume
LIN q,
a,
b
;
contradiction
then consider A being
Subset of
AS such that A13:
(
A is
being_line &
q in A )
and A14:
a in A
and A15:
b in A
by AFF_1:21;
M = A
by A1, A3, A6, A9, A13, A14, AFF_1:18;
hence
contradiction
by A2, A4, A7, A10, A13, A15, AFF_1:18;
verum
end;
( LIN q,b,b9 & a,b // a9,b9 )
by A2, A4, A5, A8, A10, AFF_1:4, AFF_1:21;
hence
q = b9
by A11, A12, AFF_1:55; verum