set A = VERUM ;
take (#) VERUM ; :: thesis: (#) VERUM is necessitive
take VERUM ; :: according to MODAL_1:def 18 :: thesis: (#) VERUM = (#) VERUM
thus (#) VERUM = (#) VERUM ; :: thesis: verum