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
A1: a in Y1 and
A2: X '||' Y1 and
A3: Y1 is being_plane and
A4: a in Y2 and
A5: X '||' Y2 and
A6: Y2 is being_plane ; :: thesis: Y1 = Y2
Y1 '||' Y2 by B1, A2, A3, A5, A6, Th61;
hence Y1 = Y2 by A1, A3, A4, A6, Lm13; :: thesis: verum