let CLSP be proper CollSp; :: thesis: for a, b being Point of CLSP st a = b holds
Line a,b = the carrier of CLSP
let a, b be Point of CLSP; :: thesis: ( a = b implies Line a,b = the carrier of CLSP )
assume A1: a = b ; :: thesis: Line a,b = the carrier of CLSP
for x being set holds
( x in Line a,b iff x in the carrier of CLSP )

proof

let x be set ; :: thesis: ( x in Line a,b iff x in the carrier of CLSP )
thus ( x in Line a,b implies x in the carrier of CLSP ) :: thesis: ( x in the carrier of CLSP implies x in Line a,b )

proof

assume x in Line a,b ; :: thesis: x in the carrier of CLSP
then ex p being Point of CLSP st
( x = p & a,b,p is_collinear ) ;
then reconsider x = x as Point of CLSP ;
x is Element of CLSP ;
hence x in the carrier of CLSP ; :: thesis: verum

end;

thus ( x in the carrier of CLSP implies x in Line a,b ) :: thesis: verum

proof

assume x in the carrier of CLSP ; :: thesis: x in Line a,b
then reconsider x = x as Point of CLSP ;
a,b,x is_collinear by A1, Th7;
hence x in Line a,b ; :: thesis: verum

end;

end;

hence Line a,b = the carrier of CLSP by TARSKI:2; :: thesis: verum