theorem Th18: :: WAYBEL10:18

for L being complete LATTICE
for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)