:: deftheorem defines -freeCountableSet FOMODEL0:def 26 :
for X being set holds X -freeCountableSet = [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:];