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 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 ; :: thesis: Y1 = Y2
Y1 '||' Y2 by A1, A3, A4, A6, A7, Th61;
hence Y1 = Y2 by A2, A4, A5, A7, Lm13; :: thesis: verum