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

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

proof

u = @ u
;
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;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

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