let U be Universe; :: thesis: for c being set st c in card U holds
card (bool c) in U
let c be set ; :: thesis: ( c in card U implies card (bool c) in U )
assume c in card U ; :: thesis: card (bool c) in U
then reconsider c = c as Element of U by CLASSES2:13;
card (bool c) in U by CLASSES4:29;
hence card (bool c) in U ; :: thesis: verum