per cases ( |.a.| = 0 or |.a.| = 1 ) by Def3;

suppose |.a.| = 0 ; :: thesis: 1 - |.a.| is weightless

hence 1 - |.a.| is weightless ; :: thesis: verum

end;

suppose |.a.| = 1 ; :: thesis: 1 - |.a.| is weightless

hence 1 - |.a.| is weightless ; :: thesis: verum

end;

end;