:: deftheorem defines code ZF_FUND1:def 4 :
for A being Subset of VAR holds code A = (decode ") .: A;