let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p being POINT of S holds
( p out a,b iff ( Collinear a,p,b & not between a,p,b ) )
let a, b, p be POINT of S; :: thesis: ( p out a,b iff ( Collinear a,p,b & not between a,p,b ) )
( p out a,b implies ( Collinear a,p,b & not between a,p,b ) )
proof
assume A1: p out a,b ; :: thesis: ( Collinear a,p,b & not between a,p,b )
( between p,b,a implies ( Collinear a,p,b & not between a,p,b ) )
proof
assume between p,b,a ; :: thesis: ( Collinear a,p,b & not between a,p,b )
hence Collinear a,p,b ; :: thesis: not between a,p,b
thus not between a,p,b :: thesis: verum
proof
assume A2: between a,p,b ; :: thesis: contradiction
then between b,p,a by Satz3p2;
hence contradiction by A1, A2, Satz3p4; :: thesis: verum
end;
end;
hence ( Collinear a,p,b & not between a,p,b ) by Satz3p2, Satz3p4, A1; :: thesis: verum
end;
hence ( p out a,b iff ( Collinear a,p,b & not between a,p,b ) ) by Satz3p1, Satz3p2; :: thesis: verum