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 object holds
( x in Line (a,b) iff x in the carrier of CLSP )

proof

let x be object ; :: 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 are_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 are_collinear by A1, Th2;
hence x in Line (a,b) ; :: thesis: verum

end;

end;

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