let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

( 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

A18:
LIN q,b,b
by AFF_1:7;
assume
LIN q,a,b
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

( 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; :: thesis: verum