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

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