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)

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

hence
(A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)
; :: thesis: verum
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 ` ) )

( V2 meets B & V2 meets B ` )

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

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

( V2 meets B & V2 meets B ` )

proof

then
( for V1 being Subset of FMT st V1 in U_FMT x holds
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 ` ) )

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

end;

hence
( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
; :: thesis: verumnow :: 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 ` ) ) ) )end;

hence
( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
; :: thesis: verumper cases
( ( W meets A & W meets A ` ) or ( W meets B & W meets B ` ) )
by A3, A8;

end;

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;hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A11; :: thesis: verum

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;hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A10; :: thesis: verum

( 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