for S being reflexive antisymmetric with_suprema with_infima RelStr
for T being antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
T is distributive