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