let V be RealLinearSpace; :: thesis: for p1, p2 being Point of V holds Line (p1,p2) = (halfline (p1,p2)) \/ (halfline (p2,p1))
let p1, p2 be Point of V; :: thesis: Line (p1,p2) = (halfline (p1,p2)) \/ (halfline (p2,p1))
thus Line (p1,p2) c= (halfline (p1,p2)) \/ (halfline (p2,p1)) :: according to XBOOLE_0:def 10 :: thesis: (halfline (p1,p2)) \/ (halfline (p2,p1)) c= Line (p1,p2)

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Line (p1,p2) or e in (halfline (p1,p2)) \/ (halfline (p2,p1)) )
assume e in Line (p1,p2) ; :: thesis: e in (halfline (p1,p2)) \/ (halfline (p2,p1))
then consider r being Real such that
A1: e = ((1 - r) * p1) + (r * p2) ;

now :: thesis: ( ( r >= 0 & e in halfline (p1,p2) ) or ( r <= 0 & e in halfline (p2,p1) ) )

per cases ( r >= 0 or r <= 0 ) ;

case r >= 0 ; :: thesis: e in halfline (p1,p2)

hence e in halfline (p1,p2) by A1; :: thesis: verum

end;

case r <= 0 ; :: thesis: e in halfline (p2,p1)

then A2: 1 - r >= 0 ;
e = ((1 - (1 - r)) * p2) + ((1 - r) * p1) by A1;
hence e in halfline (p2,p1) by A2; :: thesis: verum

end;

end;

end;

hence e in (halfline (p1,p2)) \/ (halfline (p2,p1)) by XBOOLE_0:def 3; :: thesis: verum

end;

( 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; :: thesis: verum