environ
vocabularies HIDDEN, XBOOLE_0, TARSKI;
notations HIDDEN, TARSKI, XBOOLE_0;
definitions XBOOLE_0, TARSKI;
theorems XBOOLE_0, TARSKI;
schemes ;
registrations ;
constructors HIDDEN, TARSKI, XBOOLE_0;
requirements HIDDEN;
equalities XBOOLE_0;
expansions TARSKI;
Lm1:
for X being set st X is empty holds
X = {}
:: "requirements BOOLE" is included in the environment description
:: of an article. They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Statements which cannot be expressed in Mizar language are commented out.