let P, Q be PLANE of S; :: thesis: ( K on P & L on P & K on Q & L on Q implies P = Q )
assume A3: ( K on P & L on P & K on Q & L on Q ) ; :: thesis: P = Q
consider P1 being PLANE of S such that
A4: for P2 being PLANE of S holds
( ( K on P2 & L on P2 ) iff P1 = P2 ) by A1, A2, Th49;
( P = P1 & Q = P1 ) by A3, A4;
hence P = Q ; :: thesis: verum