theorem Th13: :: CLASSES4:13

for X being set st X is axiom_GU1 & X is axiom_GU3 holds
( ( for y being set
for x being Subset of y st y in X holds
x in X ) & ( for x, y being set st x c= y & y in X holds
x in X ) & ( not X is empty implies {} in X ) )