consider cB1 being filter_base of X1 such that
A1: <.cB1.) = cF1 by Th24;
consider cB2 being filter_base of X2 such that
A2: <.cB2.) = cF2 by Th24;
<.[:cB1,cB2:].) is Filter of [:X1,X2:] ;
hence ex b₁ being Filter of [:X1,X2:] ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & b₁ = <.[:cB1,cB2:].) ) by A1, A2; :: thesis: verum