A7: bool u c= the carrier of (NormForm A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool u or x in the carrier of (NormForm A) )
assume x in bool u ; :: thesis: x in the carrier of (NormForm A)
then x is Element of (NormForm A) by Th5;
hence x in the carrier of (NormForm A) ; :: thesis: verum

end;

u = @ u ;
hence bool u is Element of Fin the carrier of (NormForm A) by A7, FINSUB_1:def 5; :: thesis: verum