let a, b be Point of TarskiEuclid2Space; :: thesis: ( between a,a,b & between a,b,b )
Tn2TR a in LSeg ((Tn2TR a),(Tn2TR b)) by RLTOPSP1:68;
hence between a,a,b by ThConv6; :: thesis: between a,b,b
Tn2TR b in LSeg ((Tn2TR a),(Tn2TR b)) by RLTOPSP1:68;
hence between a,b,b by ThConv6; :: thesis: verum