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