:: deftheorem Def2 defines join-closed WAYBEL23:def 2 :
for L being non empty RelStr
for S being Subset of L holds
( S is join-closed iff subrelstr S is join-inheriting );