reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
A12: bool u c= the carrier of (SubstLatt (V,C))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool u or x in the carrier of (SubstLatt (V,C)) )
assume x in bool u ; :: thesis: x in the carrier of (SubstLatt (V,C))
then x is Element of (SubstLatt (V,C)) by Th17;
hence x in the carrier of (SubstLatt (V,C)) ; :: thesis: verum
end;
u9 is finite ;
hence bool u is Element of Fin the carrier of (SubstLatt (V,C)) by A12, FINSUB_1:def 5; :: thesis: verum