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