let P, Q be PLANE of S; :: thesis: ( A on P & L on P & A on Q & L on Q implies P = Q )
assume that
A4: ( A on P & L on P ) and
A5: ( A on Q & L on Q ) ; :: thesis: P = Q
consider P1 being PLANE of S such that
A6: for P2 being PLANE of S holds
( ( A on P2 & L on P2 ) iff P1 = P2 ) by A1, Th26;
P1 = P by A4, A6;
hence P = Q by A5, A6; :: thesis: verum