let AS be AffinSpace; for M, N being Subset of
for o, a, b, c, a', b', c' being Element of st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b' & o <> c' & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & ( a = b or b = c or a = c ) holds
a,c' // c,a'
let M, N be Subset of ; for o, a, b, c, a', b', c' being Element of st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b' & o <> c' & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & ( a = b or b = c or a = c ) holds
a,c' // c,a'
let o, a, b, c, a', b', c' be Element of ; ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b' & o <> c' & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & ( a = b or b = c or a = c ) implies a,c' // c,a' )
assume that
A1:
M is being_line
and
A2:
N is being_line
and
A3:
M <> N
and
A4:
o in M
and
A5:
o in N
and
A6:
o <> b
and
A7:
o <> b'
and
A8:
o <> c'
and
A9:
b in M
and
A10:
c in M
and
A11:
a' in N
and
A12:
b' in N
and
A13:
c' in N
and
A14:
a,b' // b,a'
and
A15:
b,c' // c,b'
and
A16:
( a = b or b = c or a = c )
; a,c' // c,a'
A17:
c <> b'
by A1, A2, A3, A4, A5, A7, A10, A12, AFF_1:30;
now assume A18:
a = c
;
a,c' // c,a'then
b,
c' // b,
a'
by A14, A15, A17, AFF_1:14;
then
a' = c'
by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, AFF_4:9;
hence
a,
c' // c,
a'
by A18, AFF_1:11;
verum end;
hence
a,c' // c,a'
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, AFF_4:9; verum