let U be Universe; :: thesis: for c1, c2 being Cardinal st c1 in card U & c2 in card U holds
card (bool [:c1,c2:]) in U
let c1, c2 be Cardinal; :: thesis: ( c1 in card U & c2 in card U implies card (bool [:c1,c2:]) in U )
assume that
A1: c1 in card U and
A2: c2 in card U ; :: thesis: card (bool [:c1,c2:]) in U
reconsider c1 = c1, c2 = c2 as Element of U by A1, A2, CLASSES2:13;
reconsider c = bool [:c1,c2:] as Element of U ;
card c in U by CLASSES4:29;
hence card (bool [:c1,c2:]) in U ; :: thesis: verum