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

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

hence
K c= mi K
by Lm5; :: thesis: veruma 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;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