let FMT be non empty FMT_Space_Str ; :: thesis: for A, B being Subset of FMT st ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) holds
(A \/ B) ^Fodelta c= (A ^Fodelta ) \/ (B ^Fodelta )
let A, B be Subset of FMT; :: thesis: ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) implies (A \/ B) ^Fodelta c= (A ^Fodelta ) \/ (B ^Fodelta ) )
assume A1: for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ; :: thesis: (A \/ B) ^Fodelta c= (A ^Fodelta ) \/ (B ^Fodelta )
for x being Element of FMT st x in (A \/ B) ^Fodelta holds
x in (A ^Fodelta ) \/ (B ^Fodelta )

proof

let x be Element of FMT; :: thesis: ( x in (A \/ B) ^Fodelta implies x in (A ^Fodelta ) \/ (B ^Fodelta ) )
assume A2: x in (A \/ B) ^Fodelta ; :: thesis: x in (A ^Fodelta ) \/ (B ^Fodelta )
A3: for W1 being Subset of FMT holds
( not W1 in U_FMT x or ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) )

proof

let W1 be Subset of FMT; :: thesis: ( not W1 in U_FMT x or ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) )
assume A4: W1 in U_FMT x ; :: thesis: ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) )
then W1 meets A \/ B by A2, Th20;
then A5: W1 /\ (A \/ B) <> {} by XBOOLE_0:def 7;
W1 meets (A \/ B) ` by A2, A4, Th20;
then A6: W1 /\ ((A \/ B) ` ) <> {} by XBOOLE_0:def 7;
A7: (W1 /\ A) \/ (W1 /\ B) <> {} by A5, XBOOLE_1:23;
W1 /\ ((A ` ) /\ (B ` )) <> {} by A6, XBOOLE_1:53;
then ( (W1 /\ (A ` )) /\ (B ` ) <> {} & (W1 /\ (B ` )) /\ (A ` ) <> {} ) by XBOOLE_1:16;
then A8: ( W1 /\ (A ` ) meets B ` & W1 /\ (B ` ) meets A ` ) by XBOOLE_0:def 7;
then consider z1 being set such that
A9: z1 in (W1 /\ (A ` )) /\ (B ` ) by XBOOLE_0:4;
consider z2 being set such that
A10: z2 in (W1 /\ (B ` )) /\ (A ` ) by A8, XBOOLE_0:4;
( ( W1 /\ A <> {} & W1 /\ (A ` ) <> {} ) or ( W1 /\ B <> {} & W1 /\ (B ` ) <> {} ) ) by A7, A9, A10;
hence ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) by XBOOLE_0:def 7; :: thesis: verum

end;

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x & not ( V1 meets A & V1 meets A ` ) holds
( V2 meets B & V2 meets B ` )

proof

let V1, V2 be Subset of FMT; :: thesis: ( V1 in U_FMT x & V2 in U_FMT x & not ( V1 meets A & V1 meets A ` ) implies ( V2 meets B & V2 meets B ` ) )
assume ( V1 in U_FMT x & V2 in U_FMT x ) ; :: thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
then consider W being Subset of FMT such that
A11: W in U_FMT x and
A12: W c= V1 /\ V2 by A1;
( V1 /\ V2 c= V1 & V1 /\ V2 c= V2 ) by XBOOLE_1:17;
then ( W c= V1 & W c= V2 ) by A12, XBOOLE_1:1;
then A13: ( W /\ A c= V1 /\ A & W /\ (A ` ) c= V1 /\ (A ` ) & W /\ B c= V2 /\ B & W /\ (B ` ) c= V2 /\ (B ` ) ) by XBOOLE_1:26;
( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )

proof

now

per cases ( ( W meets A & W meets A ` ) or ( W meets B & W meets B ` ) ) by A3, A11;

case A14: ( W meets A & W meets A ` ) ; :: thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )

then consider z1 being set such that
A15: z1 in W /\ A by XBOOLE_0:4;
consider z2 being set such that
A16: z2 in W /\ (A ` ) by A14, XBOOLE_0:4;
thus ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A13, A15, A16, XBOOLE_0:4; :: thesis: verum

end;

case A17: ( W meets B & W meets B ` ) ; :: thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )

then consider z3 being set such that
A18: z3 in W /\ B by XBOOLE_0:4;
consider z4 being set such that
A19: z4 in W /\ (B ` ) by A17, XBOOLE_0:4;
thus ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A13, A18, A19, XBOOLE_0:4; :: thesis: verum

end;

end;

end;

hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ; :: thesis: verum

end;

hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ; :: thesis: verum

end;

then ( for V1 being Subset of FMT st V1 in U_FMT x holds
( V1 meets A & V1 meets A ` ) or for V2 being Subset of FMT st V2 in U_FMT x holds
( V2 meets B & V2 meets B ` ) ) ;
then ( x in A ^Fodelta or x in B ^Fodelta ) ;
hence x in (A ^Fodelta ) \/ (B ^Fodelta ) by XBOOLE_0:def 3; :: thesis: verum

end;

hence (A \/ B) ^Fodelta c= (A ^Fodelta ) \/ (B ^Fodelta ) by SUBSET_1:7; :: thesis: verum