take [#] COMPLEX ; :: thesis: [#] COMPLEX is symmetrical
let x be Complex; :: according to FUNCT_8:def 1 :: thesis: ( x in [#] COMPLEX implies - x in [#] COMPLEX )
thus ( x in [#] COMPLEX implies - x in [#] COMPLEX ) by XCMPLX_0:def 2; :: thesis: verum