(a | L) . 0 = a by Th28;
then a | L <> 0_. L by FUNCOP_1:7;
hence not a | L is zero by UPROOTS:def 5; :: thesis: verum