(1._ L) `1 <> 0_. L by XTUPLE_0:def 2;
hence not 1._ L is zero by defzerrat; :: thesis: verum