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

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