let P, Q be PLANE of S; :: thesis: ( K on P & L on P & K on Q & L on Q implies P = Q )

assume that

A3: ( K on P & L on P ) and

A4: ( K on Q & L on Q ) ; :: thesis: P = Q

consider P1 being PLANE of S such that

A5: for P2 being PLANE of S holds

( ( K on P2 & L on P2 ) iff P1 = P2 ) by A1, A2, Th27;

P = P1 by A3, A5;

hence P = Q by A4, A5; :: thesis: verum

assume that

A3: ( K on P & L on P ) and

A4: ( K on Q & L on Q ) ; :: thesis: P = Q

consider P1 being PLANE of S such that

A5: for P2 being PLANE of S holds

( ( K on P2 & L on P2 ) iff P1 = P2 ) by A1, A2, Th27;

P = P1 by A3, A5;

hence P = Q by A4, A5; :: thesis: verum