:: deftheorem defines Is GTARSKI4:def 7 :
for S being non empty TarskiGeometryStruct
for A, B being Subset of S
for x being POINT of S holds
( A,B Is x iff ( A is_line & B is_line & A <> B & x in A & x in B ) );