for AS being AffinSpace
for a being Element of AS
for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & a in Y & X '||' Y holds
X = Y by Lm13;