let p, q, r be POINT of TarskiEuclid2Space; :: thesis: ( between p,q,r iff Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) )
hereby :: thesis: ( Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) implies between p,q,r )
assume between p,q,r ; :: thesis: Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r))
then q is_Between p,r by GTARSKI1:def 15;
hence Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) by ThConv5; :: thesis: verum
end;
assume Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) ; :: thesis: between p,q,r
then q is_Between p,r by ThConv5;
hence between p,q,r by GTARSKI1:def 15; :: thesis: verum