(card Y) / (card (X \/ Y)) in [.0,1.]

proof

card Y <= card (X \/ Y) by NAT_1:43, XBOOLE_1:7;
then (card Y) / (card (X \/ Y)) <= 1 by XREAL_1:183;
hence (card Y) / (card (X \/ Y)) in [.0,1.] by XXREAL_1:1; :: thesis: verum

end;

hence ( ( X \/ Y <> {} implies (card Y) / (card (X \/ Y)) is Element of [.0,1.] ) & ( not X \/ Y <> {} implies 1 is Element of [.0,1.] ) ) by XXREAL_1:1; :: thesis: verum