let S be SubRelStr of L; :: thesis: ( S is closure implies not S is empty )
assume A1: S is closure ; :: thesis: not S is empty
ex_inf_of {} S,L by YELLOW_0:17;
hence not S is empty by A1, YELLOW_0:def 18; :: thesis: verum