consider x being Loop of t;
x in Loops t by Def1;
hence not Loops t is empty ; :: thesis: verum