reconsider u' = u as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
A8: u' is finite ;
bool u c= the carrier of (SubstLatt V,C)

proof

let x be set ; :: 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 Th22;
hence x in the carrier of (SubstLatt V,C) ; :: thesis: verum

end;

hence bool u is Element of Fin the carrier of (SubstLatt V,C) by A8, FINSUB_1:def 5; :: thesis: verum