theorem Th5: :: WAYBEL_7:5

for X being set
for a being Element of (BoolePoset X) holds 'not' a = X \ a