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