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

proof

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

end;

hence (card ((X `) \/ Y)) / (card ([#] R)) is Element of [.0,1.] ; :: thesis: verum