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 & a9 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 & a = a9 holds
b = 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 & a9 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 & a = a9 holds
b = b9
let M, N be Subset of AS; ( q in M & q in N & a in M & a9 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 & a = a9 implies b = b9 )
assume that
A1:
q in M
and
A2:
q in N
and
A3:
a in M
and
A4:
a9 in M
and
A5:
b in N
and
A6:
b9 in N
and
A7:
q <> a
and
A8:
( q <> b & M <> N )
and
A9:
( a,b // a9,b9 or b,a // b9,a9 )
and
A10:
M is being_line
and
A11:
N is being_line
and
A12:
a = a9
; b = b9
A13:
( a,b // a9,b & a,b // a9,b9 )
by A9, A12, AFF_1:2, AFF_1:4;
A14:
not LIN q,a,b
proof
assume
LIN q,
a,
b
;
contradiction
then consider A being
Subset of
AS such that A15:
(
A is
being_line &
q in A )
and A16:
a in A
and A17:
b in A
by AFF_1:21;
M = A
by A1, A3, A7, A10, A15, A16, AFF_1:18;
hence
contradiction
by A2, A5, A8, A11, A15, A17, AFF_1:18;
verum
end;
A18:
LIN q,b,b
by AFF_1:7;
( LIN q,a,a9 & LIN q,b,b9 )
by A1, A2, A3, A4, A5, A6, A10, A11, AFF_1:21;
hence
b = b9
by A14, A18, A13, AFF_1:56; verum