let a be Complex; :: thesis: |.(Re a).| + |.(Im a).| >= |.a.|
|.((Im a) * <i>).| = |.(Im a).| * |.<i>.| by COMPLEX1:65
.= |.(Im a).| by COMPLEX1:49 ;
then |.((Re a) + ((Im a) * <i>)).| <= |.(Re a).| + |.(Im a).| by COMPLEX1:56;
hence |.(Re a).| + |.(Im a).| >= |.a.| by COMPLEX1:13; :: thesis: verum