reconsider p = [3,0] as MP-variable by ZFMISC_1:105;
take @ p ; :: thesis: @ p is atomic
take p ; :: according to MODAL_1:def 16 :: thesis: @ p = @ p
thus @ p = @ p ; :: thesis: verum