let V, C be set ; :: thesis: for K being Element of SubstitutionSet (V,C) holds mi K = K
let K be Element of SubstitutionSet (V,C); :: thesis: mi K = K
thus mi K c= K by Th8; :: according to XBOOLE_0:def 10 :: thesis: K c= mi K

now :: thesis: for a being set st a in K holds
a in mi K

let a be set ; :: thesis: ( a in K implies a in mi K )
assume A1: a in K ; :: thesis: a in mi K
then ( a is finite & ( for b being finite set st b in K & b c= a holds
b = a ) ) by Lm1, Th5;
hence a in mi K by A1, Th7; :: thesis: verum

end;

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