let x be LINE of CPS; :: thesis: x is Subset of CPS
x c= the carrier of CPS

proof

consider a, b being Point of CPS such that
a <> b and
A1: x = Line a,b by COLLSP:def 7;

now

let z be set ; :: thesis: ( z in x implies z in the carrier of CPS )
assume z in x ; :: thesis: z in the carrier of CPS
then z in { p where p is Point of CPS : a,b,p is_collinear } by A1, COLLSP:def 5;
then ex p being Point of CPS st
( z = p & a,b,p is_collinear ) ;
hence z in the carrier of CPS ; :: thesis: verum

end;

hence x c= the carrier of CPS by TARSKI:def 3; :: thesis: verum

end;

hence x is Subset of CPS ; :: thesis: verum