let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: 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) = half-space3 (A,a)
let a, b be POINT of S; :: thesis: 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) = half-space3 (A,a)
let A be Subset of S; :: thesis: ( A is_plane & not a in A & not b in A & b in half-space3 (A,a) implies half-space3 (A,b) = half-space3 (A,a) )
assume that
A1: A is_plane and
A2: not a in A and
A3: not b in A and
A4: b in half-space3 (A,a) ; :: thesis: half-space3 (A,b) = half-space3 (A,a)
half-space3 (A,a) c= half-space3 (A,b)

proof

a in half-space3 (A,b) by A1, A2, A3, A4, Th81;
hence half-space3 (A,a) c= half-space3 (A,b) by A1, A2, A3, Th82; :: thesis: verum

end;

hence half-space3 (A,b) = half-space3 (A,a) by A1, A2, A3, A4, Th82; :: thesis: verum