take
[#] REAL
; :: thesis: [#] REAL is symmetrical

let x be Complex; :: according to FUNCT_8:def 1 :: thesis: ( x in [#] REAL implies - x in [#] REAL )

for x being Real st x in REAL holds

- x in REAL by XREAL_0:def 1;

hence ( x in [#] REAL implies - x in [#] REAL ) ; :: thesis: verum

let x be Complex; :: according to FUNCT_8:def 1 :: thesis: ( x in [#] REAL implies - x in [#] REAL )

for x being Real st x in REAL holds

- x in REAL by XREAL_0:def 1;

hence ( x in [#] REAL implies - x in [#] REAL ) ; :: thesis: verum