A1: {} is symmetrical ;
thus for b₁ being Relation st b₁ is empty holds
b₁ is with_symmetrical_domain by A1; :: thesis: verum