let AS be AffinSpace; :: thesis: for a, b being Element of
for A being Subset of st ( a,b // A or b,a // A ) & a in A holds
b in A
let a, b be Element of ; :: thesis: for A being Subset of st ( a,b // A or b,a // A ) & a in A holds
b in A
let A be Subset of ; :: thesis: ( ( a,b // A or b,a // A ) & a in A implies b in A )
assume that
A1: ( a,b // A or b,a // A ) and
A2: a in A ; :: thesis: b in A
( a,b // A & A is being_line ) by A1, AFF_1:40, AFF_1:48;
hence b in A by A2, AFF_1:37; :: thesis: verum