AA: card (X /\ Y) <= card X by NAT_1:43, XBOOLE_1:17;
(card (X /\ Y)) / (card X) <= 1 by AA, XREAL_1:185;
hence ( ( X <> {} implies (card (X /\ Y)) / (card X) is Element of [.0,1.] ) & ( not X <> {} implies 1 is Element of [.0,1.] ) ) by XXREAL_1:1; :: thesis: verum