let S be 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_line & not a in A & not b in A & b in half-plane (A,a) holds
half-plane (A,b) = half-plane (A,a)
let a, b be POINT of S; for A being Subset of S st A is_line & not a in A & not b in A & b in half-plane (A,a) holds
half-plane (A,b) = half-plane (A,a)
let A be Subset of S; ( A is_line & not a in A & not b in A & b in half-plane (A,a) implies half-plane (A,b) = half-plane (A,a) )
assume that
A1:
A is_line
and
A2:
not a in A
and
A3:
not b in A
and
A4:
b in half-plane (A,a)
; half-plane (A,b) = half-plane (A,a)
a in half-plane (A,b)
by A1, A2, A3, A4, Th21;
hence
half-plane (A,b) = half-plane (A,a)
by A4, Th22; verum