let X be OrtAfPl; :: thesis: for a, b, c, d being Element of X
for M being Subset of X
for M9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #)
for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b

let a, b, c, d be Element of X; :: thesis: for M being Subset of X
for M9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #)
for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b

let M be Subset of X; :: thesis: for M9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #)
for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b

let M9 be Subset of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b

let c9, d9 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ( c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 implies c,d // a,b )
assume that
A1: c = c9 and
A2: d = d9 and
A3: M = M9 and
A4: a in M and
A5: b in M and
A6: c9,d9 // M9 ; :: thesis: c,d // a,b
reconsider a9 = a, b9 = b as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
A7: M9 is being_line by ;
then a9,b9 // M9 by ;
then c9,d9 // a9,b9 by ;
hence c,d // a,b by ; :: thesis: verum