let P, Q, R be Point of TarskiEuclid2Space; :: thesis: ( between P,Q,R & Tn2TR P in inside_of_circle (0,0,1) & Tn2TR R in inside_of_circle (0,0,1) implies Tn2TR Q in inside_of_circle (0,0,1) )
assume that
A1: between P,Q,R and
A2: ( Tn2TR P in inside_of_circle (0,0,1) & Tn2TR R in inside_of_circle (0,0,1) ) ; :: thesis: Tn2TR Q in inside_of_circle (0,0,1)
LSeg ((Tn2TR P),(Tn2TR R)) c= inside_of_circle (0,0,1) by A2, RLTOPSP1:22;
hence Tn2TR Q in inside_of_circle (0,0,1) by A1, GTARSKI2:20; :: thesis: verum