theorem :: BOOLE:6

for X being set st X is empty holds
X = {} by Lm1;