let X be OrtAfPl; :: thesis: for a, b, c, d being Element of X
for M being Subset of X
for M' being Subset of (Af X)
for c', d' being Element of (Af X) st c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' holds
c,d // a,b
let a, b, c, d be Element of X; :: thesis: for M being Subset of X
for M' being Subset of (Af X)
for c', d' being Element of (Af X) st c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' holds
c,d // a,b
let M be Subset of X; :: thesis: for M' being Subset of (Af X)
for c', d' being Element of (Af X) st c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' holds
c,d // a,b
let M' be Subset of (Af X); :: thesis: for c', d' being Element of (Af X) st c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' holds
c,d // a,b
let c', d' be Element of (Af X); :: thesis: ( c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' implies c,d // a,b )
assume A1: ( c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' ) ; :: thesis: c,d // a,b
reconsider a' = a, b' = b as Element of (Af X) by ANALMETR:47;
A2: M' is being_line by A1, AFF_1:40;
then a',b' // M' by A1, AFF_1:66;
then c',d' // a',b' by A1, A2, AFF_1:45;
hence c,d // a,b by A1, ANALMETR:48; :: thesis: verum