theorem Th48:
for
AS being
AffinSpace for
M,
N being
Subset of
AS for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AS st
M is
being_line &
N is
being_line &
M <> N &
o in M &
o in N &
o <> b &
o <> b9 &
o <> c9 &
b in M &
c in M &
a9 in N &
b9 in N &
c9 in N &
a,
b9 // b,
a9 &
b,
c9 // c,
b9 & (
a = b or
b = c or
a = c ) holds
a,
c9 // c,
a9