theorem :: YELLOW10:65

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