let FMT be non empty FMT_Space_Str ; :: 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 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )

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 ) ) implies for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )

( 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) ^Fob <> (A ^Fob) \/ (B ^Fob) )

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 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) by A1; :: 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 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )

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 ) ) implies for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )

proof

( ex x being Element of FMT ex V1, V2 being Subset of FMT st
assume A2:
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: for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)

let A, B be Subset of FMT; :: thesis: (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)

for x being Element of FMT holds

( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) )

end;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: for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)

let A, B be Subset of FMT; :: thesis: (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)

for x being Element of FMT holds

( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) )

proof

hence
(A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)
by SUBSET_1:3; :: thesis: verum
let x be Element of FMT; :: thesis: ( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) )

A3: ( x in (A \/ B) ^Fob implies x in (A ^Fob) \/ (B ^Fob) )

end;A3: ( x in (A \/ B) ^Fob implies x in (A ^Fob) \/ (B ^Fob) )

proof

( x in (A ^Fob) \/ (B ^Fob) implies x in (A \/ B) ^Fob )
assume A4:
x in (A \/ B) ^Fob
; :: thesis: x in (A ^Fob) \/ (B ^Fob)

A5: for W1 being Subset of FMT holds

( not W1 in U_FMT x or W1 meets A or W1 meets B )

V2 meets B

V1 meets A or for V2 being Subset of FMT st V2 in U_FMT x holds

V2 meets B ) ;

then ( x in A ^Fob or x in B ^Fob ) ;

hence x in (A ^Fob) \/ (B ^Fob) by XBOOLE_0:def 3; :: thesis: verum

end;A5: for W1 being Subset of FMT holds

( not W1 in U_FMT x or W1 meets A or 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 holds
let W1 be Subset of FMT; :: thesis: ( not W1 in U_FMT x or W1 meets A or W1 meets B )

assume W1 in U_FMT x ; :: thesis: ( W1 meets A or W1 meets B )

then W1 meets A \/ B by A4, Th20;

then W1 /\ (A \/ B) <> {} ;

then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23;

then ( W1 /\ A <> {} or W1 /\ B <> {} ) ;

hence ( W1 meets A or W1 meets B ) ; :: thesis: verum

end;assume W1 in U_FMT x ; :: thesis: ( W1 meets A or W1 meets B )

then W1 meets A \/ B by A4, Th20;

then W1 /\ (A \/ B) <> {} ;

then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23;

then ( W1 /\ A <> {} or W1 /\ B <> {} ) ;

hence ( W1 meets A or W1 meets B ) ; :: thesis: verum

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 implies V2 meets B )

assume ( V1 in U_FMT x & V2 in U_FMT x ) ; :: thesis: ( V1 meets A or V2 meets B )

then consider W being Subset of FMT such that

A6: W in U_FMT x and

A7: W c= V1 /\ V2 by A2;

V1 /\ V2 c= V1 by XBOOLE_1:17;

then W c= V1 by A7;

then A8: W /\ A c= V1 /\ A by XBOOLE_1:26;

V1 /\ V2 c= V2 by XBOOLE_1:17;

then W c= V2 by A7;

then A9: W /\ B c= V2 /\ B by XBOOLE_1:26;

( W meets A or W meets B ) by A5, A6;

then ( W /\ A <> {} or W /\ B <> {} ) ;

then ex z1, z2 being Element of FMT st

( z1 in W /\ A or z2 in W /\ B ) by SUBSET_1:4;

hence ( V1 meets A or V2 meets B ) by A8, A9; :: thesis: verum

end;assume ( V1 in U_FMT x & V2 in U_FMT x ) ; :: thesis: ( V1 meets A or V2 meets B )

then consider W being Subset of FMT such that

A6: W in U_FMT x and

A7: W c= V1 /\ V2 by A2;

V1 /\ V2 c= V1 by XBOOLE_1:17;

then W c= V1 by A7;

then A8: W /\ A c= V1 /\ A by XBOOLE_1:26;

V1 /\ V2 c= V2 by XBOOLE_1:17;

then W c= V2 by A7;

then A9: W /\ B c= V2 /\ B by XBOOLE_1:26;

( W meets A or W meets B ) by A5, A6;

then ( W /\ A <> {} or W /\ B <> {} ) ;

then ex z1, z2 being Element of FMT st

( z1 in W /\ A or z2 in W /\ B ) by SUBSET_1:4;

hence ( V1 meets A or V2 meets B ) by A8, A9; :: thesis: verum

V1 meets A or for V2 being Subset of FMT st V2 in U_FMT x holds

V2 meets B ) ;

then ( x in A ^Fob or x in B ^Fob ) ;

hence x in (A ^Fob) \/ (B ^Fob) by XBOOLE_0:def 3; :: thesis: verum

proof

hence
( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) )
by A3; :: thesis: verum
assume A10:
x in (A ^Fob) \/ (B ^Fob)
; :: thesis: x in (A \/ B) ^Fob

(A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob by Th26;

hence x in (A \/ B) ^Fob by A10; :: thesis: verum

end;(A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob by Th26;

hence x in (A \/ B) ^Fob by A10; :: thesis: verum

( 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) ^Fob <> (A ^Fob) \/ (B ^Fob) )

proof

hence
( ( for x being Element of FMT
given x0 being Element of FMT, V1, V2 being Subset of FMT such that A11:
V1 in U_FMT x0
and

A12: V2 in U_FMT x0 and

A13: 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) ^Fob <> (A ^Fob) \/ (B ^Fob)

A14: not x0 in (V2 `) ^Fob

take V2 ` ; :: thesis: ((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob)

for W being Subset of FMT st W in U_FMT x0 holds

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

not x0 in (V1 `) ^Fob

end;A12: V2 in U_FMT x0 and

A13: 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) ^Fob <> (A ^Fob) \/ (B ^Fob)

A14: not x0 in (V2 `) ^Fob

proof

take
V1 `
; :: thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fob <> ((V1 `) ^Fob) \/ (B ^Fob)
A15:
V2 misses V2 `
by XBOOLE_1:79;

assume x0 in (V2 `) ^Fob ; :: thesis: contradiction

hence contradiction by A12, A15, Th20; :: thesis: verum

end;assume x0 in (V2 `) ^Fob ; :: thesis: contradiction

hence contradiction by A12, A15, Th20; :: thesis: verum

take V2 ` ; :: thesis: ((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob)

for W being Subset of FMT st W in U_FMT x0 holds

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

proof

then A17:
x0 in ((V1 `) \/ (V2 `)) ^Fob
;
let W be Subset of FMT; :: thesis: ( W in U_FMT x0 implies W meets (V1 `) \/ (V2 `) )

assume W in U_FMT x0 ; :: thesis: W meets (V1 `) \/ (V2 `)

then A16: not W c= V1 /\ V2 by A13;

W /\ ((V1 /\ V2) `) <> {}

end;assume W in U_FMT x0 ; :: thesis: W meets (V1 `) \/ (V2 `)

then A16: not W c= V1 /\ V2 by A13;

W /\ ((V1 /\ V2) `) <> {}

proof

hence
W /\ ((V1 `) \/ (V2 `)) <> {}
by XBOOLE_1:54; :: according to XBOOLE_0:def 7 :: thesis: verum
assume
W /\ ((V1 /\ V2) `) = {}
; :: thesis: contradiction

then W \ (V1 /\ V2) = {} by SUBSET_1:13;

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

end;then W \ (V1 /\ V2) = {} by SUBSET_1:13;

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

not x0 in (V1 `) ^Fob

proof

hence
((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob)
by A17, A14, XBOOLE_0:def 3; :: thesis: verum
A18:
V1 misses V1 `
by XBOOLE_1:79;

assume x0 in (V1 `) ^Fob ; :: thesis: contradiction

hence contradiction by A11, A18, Th20; :: thesis: verum

end;assume x0 in (V1 `) ^Fob ; :: thesis: contradiction

hence contradiction by A11, A18, Th20; :: 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 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) by A1; :: thesis: verum