let AS be AffinSpace; for a, b, a9, b9 being Element of AS
for M, N being Subset of AS st ( M // N or N // M ) & a in M & b in N & b9 in N & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 holds
b = b9
let a, b, a9, b9 be Element of AS; for M, N being Subset of AS st ( M // N or N // M ) & a in M & b in N & b9 in N & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 holds
b = b9
let M, N be Subset of AS; ( ( M // N or N // M ) & a in M & b in N & b9 in N & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 implies b = b9 )
assume that
A1:
( M // N or N // M )
and
A2:
a in M
and
A3:
( b in N & b9 in N )
and
A4:
M <> N
and
A5:
( ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 )
; b = b9
a,b // a,b9
by A5, AFF_1:4;
then
LIN a,b,b9
by AFF_1:def 1;
then A6:
LIN b,b9,a
by AFF_1:6;
assume A7:
b <> b9
; contradiction
N is being_line
by A1, AFF_1:36;
then
a in N
by A3, A6, A7, AFF_1:25;
hence
contradiction
by A1, A2, A4, AFF_1:45; verum