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 Th40; :: according to XBOOLE_0:def 10 :: thesis: K c= mi K

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in K holds
a in mi K

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 Th32;
hence a in mi K by A1, Th39; :: thesis: verum

end;

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