let FMT be non empty FMT_Space_Str ; :: thesis: ( FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) ) implies 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 ) )
assume A1: FMT is Fo_filled ; :: thesis: ( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or 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 ) )
( ex x being Element of FMT ex V1, V2 being Subset of FMT st
( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds
not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A \/ B) ^Fodelta <> (A ^Fodelta) \/ (B ^Fodelta) )
proof
given x0 being Element of FMT, V1, V2 being Subset of FMT such that A2: V1 in U_FMT x0 and
A3: V2 in U_FMT x0 and
A4: for W being Subset of FMT st W in U_FMT x0 holds
not W c= V1 /\ V2 ; :: thesis: ex A, B being Subset of FMT st (A \/ B) ^Fodelta <> (A ^Fodelta) \/ (B ^Fodelta)
take V1 ` ; :: thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fodelta <> ((V1 `) ^Fodelta) \/ (B ^Fodelta)
take V2 ` ; :: thesis: ((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta)
A5: not x0 in (V2 `) ^Fodelta
proof
assume x0 in (V2 `) ^Fodelta ; :: thesis: contradiction
then V2 meets V2 ` by A3, Th19;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
for W being Subset of FMT st W in U_FMT x0 holds
( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` )
proof
let W be Subset of FMT; :: thesis: ( W in U_FMT x0 implies ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) )
assume A6: W in U_FMT x0 ; :: thesis: ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` )
then A7: not W c= V1 /\ V2 by A4;
A8: W meets (V1 /\ V2) `
proof
assume W /\ ((V1 /\ V2) `) = {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then W \ (V1 /\ V2) = {} by SUBSET_1:13;
hence contradiction by A7, XBOOLE_1:37; :: thesis: verum
end;
( x0 in V1 & x0 in V2 ) by A1, A2, A3;
then A9: x0 in V1 /\ V2 by XBOOLE_0:def 4;
x0 in W by A1, A6;
then W /\ (((V1 /\ V2) `) `) <> {} by A9, XBOOLE_0:def 4;
then W meets ((V1 /\ V2) `) ` ;
hence ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) by A8, XBOOLE_1:54; :: thesis: verum
end;
then A10: x0 in ((V1 `) \/ (V2 `)) ^Fodelta ;
not x0 in (V1 `) ^Fodelta
proof
assume x0 in (V1 `) ^Fodelta ; :: thesis: contradiction
then V1 meets V1 ` by A2, Th19;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
hence ((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta) by A10, A5, XBOOLE_0:def 3; :: thesis: verum
end;
hence ( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or 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: verum