let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for p, q, r, s being POINT of S st p,q out s,r holds
( s <> p & s <> q & r <> p & r <> q & p <> q )
let p, q, r, s be POINT of S; :: thesis: ( p,q out s,r implies ( s <> p & s <> q & r <> p & r <> q & p <> q ) )
assume A1: p,q out s,r ; :: thesis: ( s <> p & s <> q & r <> p & r <> q & p <> q )
then ( p <> q & Line (p,q) out s,r ) ;
then ex x being POINT of S st
( between s, Line (p,q),x & between r, Line (p,q),x ) ;
hence ( s <> p & s <> q & r <> p & r <> q & p <> q ) by A1, GTARSKI3:83; :: thesis: verum