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;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x or 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 are_collinear } by A1, COLLSP:def 5;
then ex p being Point of CPS st
( z = p & a,b,p are_collinear ) ;
hence z in the carrier of CPS ; :: thesis: verum
end;
hence x is Subset of CPS ; :: thesis: verum