let Y1, Y2 be Subset of AS; :: thesis: ( 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 & X '||' Y1 & Y1 is being_plane ) and
A3: ( a in Y2 & X '||' Y2 & Y2 is being_plane ) ; :: thesis: Y1 = Y2
Y1 '||' Y2 by A1, A2, A3, Th61;
hence Y1 = Y2 by A2, A3, Lm13; :: thesis: verum