for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
{} in X