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

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