rank L > 0 ;
then rank (DualLat L) <> 0 by ThRankDL;
then (Omega). (DualLat L) <> (0). (DualLat L) by ZMODUL05:1;
hence not DualLat L is trivial by ZMODUL07:41; :: thesis: verum