let AS be AffinSpace; :: thesis: for A, P, C being Subset of
for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & ( o = a' or a = a' ) holds
b,c // b',c'
let A, P, C be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & ( o = a' or a = a' ) holds
b,c // b',c'
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & ( o = a' or a = a' ) implies b,c // b',c' )
assume that
A1: o in A and
A2: o in P and
A3: o in C and
A4: o <> a and
A5: o <> b and
A6: o <> c and
A7: a in A and
A8: b in P and
A9: b' in P and
A10: c in C and
A11: c' in C and
A12: A is being_line and
A13: P is being_line and
A14: C is being_line and
A15: A <> P and
A16: A <> C and
A17: a,b // a',b' and
A18: a,c // a',c' and
A19: ( o = a' or a = a' ) ; :: thesis: b,c // b',c'

A20: now

assume A21: a = a' ; :: thesis: b,c // b',c'
then A22: c = c' by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:9;
b = b' by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A21, AFF_4:9;
hence b,c // b',c' by A22, AFF_1:11; :: thesis: verum

end;

now

assume A23: o = a' ; :: thesis: b,c // b',c'
then A24: o = c' by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:8;
o = b' by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A23, AFF_4:8;
hence b,c // b',c' by A24, AFF_1:12; :: thesis: verum

end;

hence b,c // b',c' by A19, A20; :: thesis: verum