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

for A being Subset of AS st A is being_line holds

( a in A iff a * A = A )

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

( a in A iff a * A = A )

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

assume A1: A is being_line ; :: thesis: ( a in A iff a * A = A )

for A being Subset of AS st A is being_line holds

( a in A iff a * A = A )

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

( a in A iff a * A = A )

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

assume A1: A is being_line ; :: thesis: ( a in A iff a * A = A )

now :: thesis: ( a in A implies a * A = A )

hence
( a in A iff a * A = A )
by A1, Def3; :: thesis: verumassume 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

end;A // A by A1, AFF_1:41;

hence a * A = A by A1, A2, Def3; :: thesis: verum