let CPS be proper CollSp; :: thesis: for a' being Point of CPS ex b' being Point of CPS st a' <> b'
let a' be Point of CPS; :: thesis: ex b' being Point of CPS st a' <> b'
consider p', q', r' being Point of CPS such that
A1: p' <> q' and
q' <> r' and
r' <> p' by Th10;
( a' <> p' or a' <> q' ) by A1;
hence ex b' being Point of CPS st a' <> b' ; :: thesis: verum