for X being set
for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )