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

proof

( 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 & V2 in U_FMT x0 ) and
A3: 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 )
A4: x0 in ((V1 ` ) \/ (V2 ` )) ^Fodelta

proof

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 A5: W in U_FMT x0 ; :: thesis: ( W meets (V1 ` ) \/ (V2 ` ) & W meets ((V1 ` ) \/ (V2 ` )) ` )
then A6: not W c= V1 /\ V2 by A3;
A7: W meets (V1 /\ V2) `

proof

assume W /\ ((V1 /\ V2) ` ) = {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then W \ (V1 /\ V2) = {} by SUBSET_1:32;
hence contradiction by A6, XBOOLE_1:37; :: thesis: verum

end;

( x0 in V1 & x0 in V2 ) by A1, A2, Def8;
then A8: x0 in V1 /\ V2 by XBOOLE_0:def 4;
x0 in W by A1, A5, Def8;
then W /\ (((V1 /\ V2) ` ) ` ) <> {} by A8, XBOOLE_0:def 4;
then W meets ((V1 /\ V2) ` ) ` by XBOOLE_0:def 7;
hence ( W meets (V1 ` ) \/ (V2 ` ) & W meets ((V1 ` ) \/ (V2 ` )) ` ) by A7, XBOOLE_1:54; :: thesis: verum

end;

hence x0 in ((V1 ` ) \/ (V2 ` )) ^Fodelta ; :: thesis: verum

end;

A9: not x0 in (V1 ` ) ^Fodelta

proof

assume x0 in (V1 ` ) ^Fodelta ; :: thesis: contradiction
then V1 meets V1 ` by A2, Th20;
hence contradiction by XBOOLE_1:79; :: thesis: verum

end;

A10: not x0 in (V2 ` ) ^Fodelta

proof

assume x0 in (V2 ` ) ^Fodelta ; :: thesis: contradiction
then V2 meets V2 ` by A2, Th20;
hence contradiction by XBOOLE_1:79; :: thesis: verum

end;

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 )
thus ((V1 ` ) \/ (V2 ` )) ^Fodelta <> ((V1 ` ) ^Fodelta ) \/ ((V2 ` ) ^Fodelta ) by A4, A9, A10, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( ( 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 ) ) ; :: 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