let CLSP be CollSp; :: thesis: for a, b being Point of CLSP holds
( a in Line a,b & b in Line a,b )
let a, b be Point of CLSP; :: thesis: ( a in Line a,b & b in Line a,b )
thus a in Line a,b :: thesis: b in Line a,b

proof

a,b,a is_collinear by Th7;
hence a in Line a,b ; :: thesis: verum

end;

thus b in Line a,b :: thesis: verum

proof

a,b,b is_collinear by Th7;
hence b in Line a,b ; :: thesis: verum

end;