Algorithmic logic

Are you ready? A challenge
Given the following piece of software prove or disprove the following formula
[math] \vdash \forall_{n_0 \in Node} \forall_{e \in T}\,[\textbf{call } insert(n_0,e)]contains(n_0,e) [/math] tzn, że jest logiczną konsekwencją przyjęcia definicji klasy $BST$ iż dla każdego węzła $n_0$ i każdego elementu $e$ typu $T$ po wykonaniu instrukcji $insert(n_),e)$ zachodzi $contains(n_0,e)$.