A1: {} is symmetrical

proof

assume not {} is symmetrical ; :: thesis: contradiction
then ex x being complex number st
( x in {} & not - x in {} ) by Def1;
hence contradiction ; :: thesis: verum

end;

dom {} = {} ;
hence for b₁ being Relation st b₁ is zero holds
b₁ is with_symmetrical_domain by A1, Def2; :: thesis: verum