let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p being POINT of S st p out a,b holds
( p,a <= p,b iff between p,a,b )
let a, b, p be POINT of S; :: thesis: ( p out a,b implies ( p,a <= p,b iff between p,a,b ) )
assume A1: p out a,b ; :: thesis: ( p,a <= p,b iff between p,a,b )
A2: ( p,a <= p,b implies between p,a,b )
proof
assume A3: p,a <= p,b ; :: thesis: between p,a,b
consider y being POINT of S such that
A4: ( between p,y,b & p,a equiv p,y ) by A3;
A5: p out y,b by A1, A4, GTARSKI1:def 7;
p,y equiv p,y by Satz2p1;
hence between p,a,b by A4, A1, A5, Satz6p11pb; :: thesis: verum
end;
( between p,a,b implies p,a <= p,b )
proof
assume A6: between p,a,b ; :: thesis: p,a <= p,b
then Collinear p,a,b ;
hence p,a <= p,b by A6, Satz5p12; :: thesis: verum
end;
hence ( p,a <= p,b iff between p,a,b ) by A2; :: thesis: verum