let x be set ; :: thesis: ( x in ([:f1,f2:] /\ [:g1,g2:]) \/ [:H1,H2:] implies ( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] ) )
set y = x `1 ;
set z = x `2 ;
set x1 = (x `1) `1 ;
set x2 = (x `1) `2 ;
set x3 = (x `2) `1 ;
set x4 = (x `2) `2 ;
set xx = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]];
( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] & [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:g1,g2:] ) ) by XBOOLE_0:def 4;
then ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff ( [((x `1) `1),((x `2) `1)] in f1 & [((x `1) `1),((x `2) `1)] in g1 & [((x `1) `2),((x `2) `2)] in f2 & [((x `1) `2),((x `2) `2)] in g2 ) ) by Lm73;
then ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff ( [((x `1) `1),((x `2) `1)] in f1 /\ g1 & [((x `1) `2),((x `2) `2)] in f2 /\ g2 ) ) by XBOOLE_0:def 4;
then A1: ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:H1,H2:] ) by Lm73;
assume x in ([:f1,f2:] /\ [:g1,g2:]) \/ [:H1,H2:] ; :: thesis: ( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] )
thus ( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] ) by A1, Lm75; :: thesis: verum