let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for A, A9 being Subset of S st A is_line & A9 is_line & A <> A9 holds
ex r being POINT of S st
( not r in A & r in A9 )
let A, A9 be Subset of S; :: thesis: ( A is_line & A9 is_line & A <> A9 implies ex r being POINT of S st
( not r in A & r in A9 ) )
assume that
A1: A is_line and
A2: A9 is_line and
A3: A <> A9 ; :: thesis: ex r being POINT of S st
( not r in A & r in A9 )
consider p9, q9 being POINT of S such that
A4: p9 <> q9 and
A5: A9 = Line (p9,q9) by A2;
( not p9 in A or not q9 in A ) by A1, A3, A4, A5, GTARSKI3:87;
hence ex r being POINT of S st
( not r in A & r in A9 ) by A5, GTARSKI3:83; :: thesis: verum