theorem :: GTARSKI3:122

for S being TarskiGeometryStruct holds
( S is satisfying_BetweennessIdentity iff S is (IB) ) ;