:: deftheorem defines closure WAYBEL_1:def 14 :
for L being non empty RelStr
for c being Function of L,L holds
( c is closure iff ( c is projection & id L <= c ) );