5 in { k where k is Element of NAT : 5 <= k } ;
hence not VAR is empty ; :: thesis: verum