theorem Th22: :: CARDFIL4:23

for X1, X2 being non empty set
for cA1, cB1 being filter_base of X1
for cA2, cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2 st cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) holds
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)