(card (A /\ B)) / (card (A \/ B)) in [.0,1.]
proof
B1: A /\ B c= A by XBOOLE_1:17;
A c= A \/ B by XBOOLE_1:7;
then A /\ B c= A \/ B by B1;
then (card (A /\ B)) / (card (A \/ B)) <= 1 by XREAL_1:185, NAT_1:43;
hence (card (A /\ B)) / (card (A \/ B)) in [.0,1.] by XXREAL_1:1; :: thesis: verum
end;
hence ( ( A \/ B <> {} implies (card (A /\ B)) / (card (A \/ B)) is Element of [.0,1.] ) & ( not A \/ B <> {} implies 1 is Element of [.0,1.] ) ) by XXREAL_1:1; :: thesis: verum