theorem :: FINTOPO3:7

for T being non empty RelStr
for A, B being Subset of T holds (A /\ B) ^b c= (A ^b) /\ (B ^b)