set B = VERUM ;
set A = VERUM ;
take VERUM '&' VERUM ; :: thesis: VERUM '&' VERUM is conjunctive
take VERUM ; :: according to MODAL_1:def 19 :: thesis: ex B being MP-wff st VERUM '&' VERUM = VERUM '&' B
take VERUM ; :: thesis: VERUM '&' VERUM = VERUM '&' VERUM
thus VERUM '&' VERUM = VERUM '&' VERUM ; :: thesis: verum