:: deftheorem defines BK-model-Plane BKMODEL3:def 9 :
BK-model-Plane = TarskiGeometryStruct(# BK_model,BK-model-Betweenness,BK-model-Equidistance #);