let I be non empty non degenerated multLoopStr_0 ; :: thesis: not Q. I is empty
1. I <> 0. I ;
then [(1. I),(1. I)] in Q. I by Def1;
hence not Q. I is empty ; :: thesis: verum