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 A6, AFF_1:26;
then a9,b9 // M9 by A3, A4, A5, AFF_1:52;
then c9,d9 // a9,b9 by A7, A6, AFF_1:31;
hence c,d // a,b by A1, A2, ANALMETR:36; :: thesis: verum