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

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