theorem Th16: :: WAYBEL10:16

for L being non empty RelStr
for x being object holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )