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_{1} 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_{1} = <.[:cB1,cB2:].) )
by A1, A2; :: thesis: verum

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

( <.cB1.) = cF1 & <.cB2.) = cF2 & b