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' & q' <> r' & r' <> p' ) by Th10;
( a' <> p' or a' <> q' ) by A1;
hence ex b' being Point of CPS st a' <> b' ; :: thesis: verum