set A = VERUM ;
set B = VERUM ;
take VERUM '&' VERUM ; :: thesis: VERUM '&' VERUM is conjunctive
take VERUM ; :: according to MODAL_1:def 20 :: 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