- 0_No = [(-- (R_ 0_No)),(-- (L_ 0_No))] by Th7;
hence - 0_No = 0_No by Th22; :: thesis: verum