let V be RealLinearSpace; for p1, p2 being Point of V holds Line (p1,p2) = (halfline (p1,p2)) \/ (halfline (p2,p1))
let p1, p2 be Point of V; Line (p1,p2) = (halfline (p1,p2)) \/ (halfline (p2,p1))
thus
Line (p1,p2) c= (halfline (p1,p2)) \/ (halfline (p2,p1))
XBOOLE_0:def 10 (halfline (p1,p2)) \/ (halfline (p2,p1)) c= Line (p1,p2)
( halfline (p1,p2) c= Line (p1,p2) & halfline (p2,p1) c= Line (p1,p2) )
by Th62;
hence
(halfline (p1,p2)) \/ (halfline (p2,p1)) c= Line (p1,p2)
by XBOOLE_1:8; verum