let AS be 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
let M, N be 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
let o, a, b, c, a9, b9, c9 be Element of AS; ( 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 ) implies a,c9 // c,a9 )
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 <> b9
and
A8:
o <> c9
and
A9:
b in M
and
A10:
c in M
and
A11:
a9 in N
and
A12:
b9 in N
and
A13:
c9 in N
and
A14:
a,b9 // b,a9
and
A15:
b,c9 // c,b9
and
A16:
( a = b or b = c or a = c )
; a,c9 // c,a9
A17:
c <> b9
by A1, A2, A3, A4, A5, A7, A10, A12, AFF_1:18;
now ( a = c implies a,c9 // c,a9 )assume A18:
a = c
;
a,c9 // c,a9then
b,
c9 // b,
a9
by A14, A15, A17, AFF_1:5;
then
a9 = c9
by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, AFF_4:9;
hence
a,
c9 // c,
a9
by A18, AFF_1:2;
verum end;
hence
a,c9 // c,a9
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, AFF_4:9; verum