let CPS be proper CollSp; :: thesis: for a' being Point of ex b' being Point of st a' <> b'
let a' be Point of ; :: thesis: ex b' being Point of st a' <> b'
consider p', q', r' being Point of 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 st a' <> b' ; :: thesis: verum