theory Practicalimports Mainbegin section \Part 1\ (* 1 mark *)lemma disjunction_idempotence:“A \ A \ A”apply(rule iffI)apply(erule disjE)apply assumption+apply(rule disjI1)apply assumptiondone (* 1 mark *)lemma conjunction_idempotence:“A \ A \ A”apply(rule…