for AS being AffinSpace
for a being Element of AS
for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds
A c= X