let a be Real; :: thesis: for b being Real holds
( not |.a.| = b or a = b or a = - b )
( |.a.| = a or |.a.| = - a ) by COMPLEX1:71;
hence for b being Real holds
( not |.a.| = b or a = b or a = - b ) ; :: thesis: verum