let Y1, Y2 be Subset of AS; ( a in Y1 & X '||' Y1 & Y1 is being_plane & a in Y2 & X '||' Y2 & Y2 is being_plane implies Y1 = Y2 )
assume that
A2:
a in Y1
and
A3:
X '||' Y1
and
A4:
Y1 is being_plane
and
A5:
a in Y2
and
A6:
X '||' Y2
and
A7:
Y2 is being_plane
; Y1 = Y2
Y1 '||' Y2
by A1, A3, A4, A6, A7, Th61;
hence
Y1 = Y2
by A2, A4, A5, A7, Lm13; verum