let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S holds a,b <= a,b
let a, b be POINT of S; :: thesis: a,b <= a,b
between a,b,b by Satz3p1;
hence a,b <= a,b by Satz2p1; :: thesis: verum