theorem Th87: :: GTARSKI5:87

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d being POINT of S
for A being Subset of S st A is_plane & not Collinear a,b,c & a in A & b in A & c in A & not d in A holds
not a,b,c,d are_coplanar by Th52;