:: deftheorem Def3 defines completely-distributive WAYBEL_5:def 3 :
for L being non empty RelStr holds
( L is completely-distributive iff ( L is complete & ( for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) );