let CPS be proper CollSp; :: thesis: for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9
let a9 be Point of CPS; :: thesis: ex b9 being Point of CPS st a9 <> b9
consider p9, q9, r9 being Point of CPS such that
A1: p9 <> q9 and
q9 <> r9 and
r9 <> p9 by Th6;
( a9 <> p9 or a9 <> q9 ) by A1;
hence ex b9 being Point of CPS st a9 <> b9 ; :: thesis: verum