theorem Th82: :: GTARSKI5:82
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A is_plane & not a in A & not b in A & b in half-space3 (A,a) holds
half-space3 (A,b) c= half-space3 (A,a)