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 that
A1: c = c' and
A2: d = d' and
A3: M = M' and
A4: a in M and
A5: b in M and
A6: c',d' // M' ; :: thesis: c,d // a,b
reconsider a' = a, b' = b as Element of (Af X) by ANALMETR:47;
M' is being_line by A6, AFF_1:40;
then a',b' // M' by A3, A4, A5, AFF_1:66;
then c',d' // a',b' by A6, AFF_1:40, AFF_1:45;
hence c,d // a,b by A1, A2, ANALMETR:48; :: thesis: verum