let AS be AffinSpace; :: thesis: for a being Element of AS
for A being Subset of AS st A is being_line & a in A holds
a * A = A
let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A holds
a * A = A
let A be Subset of AS; :: thesis: ( A is being_line & a in A implies a * A = A )
assume that
A1: A is being_line and
A2: a in A ; :: thesis: a * A = A
A // A by A1, AFF_1:41;
hence a * A = A by A1, A2, Def3; :: thesis: verum