theorem Th27: :: WAYBEL10:27

for L being non empty RelStr
for x being object holds
( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )