theorem :: RLTOPSP1:78

for V being non trivial RealLinearSpace
for L being non trivial line of V ex p, q being Point of V st
( p <> q & L = Line (p,q) )