let n be Nat; :: thesis: for p1 being Point of
for A being Subset of st A is being_line holds
ex p2 being Point of st
( p1 <> p2 & p2 in A )
let p1 be Point of ; :: thesis: for A being Subset of st A is being_line holds
ex p2 being Point of st
( p1 <> p2 & p2 in A )
let A be Subset of ; :: thesis: ( A is being_line implies ex p2 being Point of st
( p1 <> p2 & p2 in A ) )
assume A is being_line ; :: thesis: ex p2 being Point of st
( p1 <> p2 & p2 in A )
then consider q1, q2 being Point of such that
A1: q1 in A and
A2: ( q2 in A & q1 <> q2 ) by Th51;
( p1 = q1 implies ( p1 <> q2 & q2 in A ) ) by A2;
hence ex p2 being Point of st
( p1 <> p2 & p2 in A ) by A1; :: thesis: verum