let R be Relation of B,A; :: thesis: R is empty
rng R = {} ;
hence R is empty ; :: thesis: verum