let AS be AffinSpace; :: thesis: for a being Element of AS

for A being Subset of AS st A is being_line holds

a * A is being_line

let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds

a * A is being_line

let A be Subset of AS; :: thesis: ( A is being_line implies a * A is being_line )

set M = a * A;

assume A is being_line ; :: thesis: a * A is being_line

then A // a * A by Def3;

hence a * A is being_line by AFF_1:36; :: thesis: verum

for A being Subset of AS st A is being_line holds

a * A is being_line

let a be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds

a * A is being_line

let A be Subset of AS; :: thesis: ( A is being_line implies a * A is being_line )

set M = a * A;

assume A is being_line ; :: thesis: a * A is being_line

then A // a * A by Def3;

hence a * A is being_line by AFF_1:36; :: thesis: verum