let AS be AffinSpace; :: thesis: for a, b, b', a' being Element of
for M, N being Subset of st ( M // N or N // M ) & a in M & b in N & b' in N & M <> N & ( a,b // a',b' or b,a // b',a' ) & a = a' holds
b = b'
let a, b, b', a' be Element of ; :: thesis: for M, N being Subset of st ( M // N or N // M ) & a in M & b in N & b' in N & M <> N & ( a,b // a',b' or b,a // b',a' ) & a = a' holds
b = b'
let M, N be Subset of ; :: thesis: ( ( M // N or N // M ) & a in M & b in N & b' in N & M <> N & ( a,b // a',b' or b,a // b',a' ) & a = a' implies b = b' )
assume that
A1: ( M // N or N // M ) and
A2: a in M and
A3: ( b in N & b' in N ) and
A4: M <> N and
A5: ( ( a,b // a',b' or b,a // b',a' ) & a = a' ) ; :: thesis: b = b'
a,b // a,b' by A5, AFF_1:13;
then LIN a,b,b' by AFF_1:def 1;
then A6: LIN b,b',a by AFF_1:15;
assume A7: b <> b' ; :: thesis: contradiction
N is being_line by A1, AFF_1:50;
then a in N by A3, A6, A7, AFF_1:39;
hence contradiction by A1, A2, A4, AFF_1:59; :: thesis: verum