let A be set ; :: thesis: for K being Element of Normal_forms_on A holds mi K = K
let K be Element of Normal_forms_on A; :: thesis: mi K = K
thus mi K c= K by Th64; :: according to XBOOLE_0:def 10 :: thesis: K c= mi K

now

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in K implies a in mi K )
assume A1: a in K ; :: thesis: a in mi K
then for b being Element of DISJOINT_PAIRS A st b in K & b c= a holds
b = a by Th52;
hence a in mi K by A1, Th61; :: thesis: verum

end;

hence K c= mi K by Lm5; :: thesis: verum