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