theorem Th12: :: FINTOPO3:12
for T being non empty RelStr
for A, B being Subset of T holds (A ^d) /\ (B ^d) = (A /\ B) ^d