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, Th19;
then W1 /\ ((A \/ B) `) <> {} ;
then A5: W1 /\ ((A `) /\ (B `)) <> {} by XBOOLE_1:53;
then (W1 /\ (A `)) /\ (B `) <> {} by XBOOLE_1:16;
then W1 /\ (A `) meets B ` ;
then A6: ex z1 being object st z1 in (W1 /\ (A `)) /\ (B `) by XBOOLE_0:4;
(W1 /\ (B `)) /\ (A `) <> {} by A5, XBOOLE_1:16;
then W1 /\ (B `) meets A ` ;
then A7: ex z2 being object st z2 in (W1 /\ (B `)) /\ (A `) by XBOOLE_0:4;
W1 meets A \/ B by A2, A4, Th19;
then W1 /\ (A \/ B) <> {} ;
then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23;
then ( ( W1 /\ A <> {} & W1 /\ (A `) <> {} ) or ( W1 /\ B <> {} & W1 /\ (B `) <> {} ) ) by A6, A7;
hence ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) ; :: 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
A8: W in U_FMT x and
A9: W c= V1 /\ V2 by A1;
V1 /\ V2 c= V2 by XBOOLE_1:17;
then W c= V2 by A9;
then A10: ( W /\ B c= V2 /\ B & W /\ (B `) c= V2 /\ (B `) ) by XBOOLE_1:26;
V1 /\ V2 c= V1 by XBOOLE_1:17;
then W c= V1 by A9;
then A11: ( W /\ A c= V1 /\ A & W /\ (A `) c= V1 /\ (A `) ) by XBOOLE_1:26;
( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
proof
now :: thesis: ( ( W meets A & W meets A ` & ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ) or ( W meets B & W meets B ` & ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ) )
per cases ( ( W meets A & W meets A ` ) or ( W meets B & W meets B ` ) ) by A3, A8;
case ( W meets A & W meets A ` ) ; :: thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
then ( ex z1 being object st z1 in W /\ A & ex z2 being object st z2 in W /\ (A `) ) by XBOOLE_0:4;
hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A11; :: thesis: verum
end;
case ( W meets B & W meets B ` ) ; :: thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
then ( ex z3 being object st z3 in W /\ B & ex z4 being object st z4 in W /\ (B `) ) by XBOOLE_0:4;
hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A10; :: 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) ; :: thesis: verum