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 between2 a,A,b holds
not A out2 a,b
let a, b be POINT of S; :: thesis: for A being Subset of S st between2 a,A,b holds
not A out2 a,b
let A be Subset of S; :: thesis: ( between2 a,A,b implies not A out2 a,b )
assume A1: between2 a,A,b ; :: thesis: not A out2 a,b
assume A out2 a,b ; :: thesis: contradiction
then between2 b,A,b by A1, Th74;
hence contradiction by GTARSKI1:def 10; :: thesis: verum