let AS be AffinSpace; :: thesis: for a being Element of AS
for A being Subset of AS st A is being_line holds
ex b being Element of AS st
( a <> b & b in A )
let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds
ex b being Element of AS st
( a <> b & b in A )
let A be Subset of AS; :: thesis: ( A is being_line implies ex b being Element of AS st
( a <> b & b in A ) )
assume A is being_line ; :: thesis: ex b being Element of AS st
( a <> b & b in A )
then consider p, q being Element of AS such that
A1: p in A and
A2: q in A and
A3: p <> q by Th18;
( a = p implies ( a <> q & q in A ) ) by A2, A3;
hence ex b being Element of AS st
( a <> b & b in A ) by A1; :: thesis: verum