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 b in half-plane (A,a) holds
half-plane (A,b) c= half-plane (A,a)
let a, b be POINT of S; :: thesis: for A being Subset of S st b in half-plane (A,a) holds
half-plane (A,b) c= half-plane (A,a)
let A be Subset of S; :: thesis: ( b in half-plane (A,a) implies half-plane (A,b) c= half-plane (A,a) )
assume b in half-plane (A,a) ; :: thesis: half-plane (A,b) c= half-plane (A,a)
then consider t being POINT of S such that
A1: b = t and
A2: A out t,a ;
half-plane (A,b) c= half-plane (A,a)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in half-plane (A,b) or x in half-plane (A,a) )
assume x in half-plane (A,b) ; :: thesis: x in half-plane (A,a)
then consider y being POINT of S such that
A3: x = y and
A4: A out y,b ;
A out y,a by A1, A2, A4, Th19;
hence x in half-plane (A,a) by A3; :: thesis: verum

end;

hence half-plane (A,b) c= half-plane (A,a) ; :: thesis: verum