( |.a.| >= 0 & |.a.| <> 0 ) by Def3;
hence |.a.| is positive ; :: thesis: verum