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) )

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

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

hence
( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or for x being Element of FMT
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

( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` )

not x0 in (V1 `) ^Fodelta

end;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

for W being Subset of FMT st W in U_FMT x0 holds
assume
x0 in (V2 `) ^Fodelta
; :: thesis: contradiction

then V2 meets V2 ` by A3, Th19;

hence contradiction by XBOOLE_1:79; :: thesis: verum

end;then V2 meets V2 ` by A3, Th19;

hence contradiction by XBOOLE_1:79; :: thesis: verum

( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` )

proof

then A10:
x0 in ((V1 `) \/ (V2 `)) ^Fodelta
;
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) `

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;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

( x0 in V1 & x0 in V2 )
by A1, A2, A3;
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;then W \ (V1 /\ V2) = {} by SUBSET_1:13;

hence contradiction by A7, XBOOLE_1:37; :: thesis: verum

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

not x0 in (V1 `) ^Fodelta

proof

hence
((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta)
by A10, A5, XBOOLE_0:def 3; :: thesis: verum
assume
x0 in (V1 `) ^Fodelta
; :: thesis: contradiction

then V1 meets V1 ` by A2, Th19;

hence contradiction by XBOOLE_1:79; :: thesis: verum

end;then V1 meets V1 ` by A2, Th19;

hence contradiction by XBOOLE_1:79; :: thesis: verum

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