I think that the following PROMELA code proofs it:

    byte n = 0
    byte A = 0
    byte B = 0
    proctype Client(byte id)
    {
        do
        :: (A == 0) -> B = id
        :: (A == id) -> 
            n = n + 1;
            assert (n <= 1);
            n = n - 1;
            A = 0
        od
    }
    proctype LockServer()
    {
        do
        :: (A == 0) -> A = B
        od
    }
    init {
        atomic {
            run LockServer();
            run Client(1);
            run Client(2);
            run Client(3);
        }
    }

It fails when two 'Client(2)' is replaced by 'Client(1)'