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

proof

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

proof

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

proof

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 )

proof

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;

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x & not V1 meets A holds
V2 meets B

proof

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;

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

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

proof

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;

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

end;

hence (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) by SUBSET_1:3; :: thesis: verum

end;

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

proof

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

proof

A15: V2 misses V2 ` by XBOOLE_1:79;
assume x0 in (V2 `) ^Fob ; :: thesis: contradiction
hence contradiction by A12, A15, Th20; :: thesis: verum

end;

take V1 ` ; :: thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fob <> ((V1 `) ^Fob) \/ (B ^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 `)

proof

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) `) <> {}

proof

assume W /\ ((V1 /\ V2) `) = {} ; :: thesis: contradiction
then W \ (V1 /\ V2) = {} by SUBSET_1:13;
hence contradiction by A16, XBOOLE_1:37; :: thesis: verum

end;

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

end;

then A17: x0 in ((V1 `) \/ (V2 `)) ^Fob ;
not x0 in (V1 `) ^Fob

proof

A18: V1 misses V1 ` by XBOOLE_1:79;
assume x0 in (V1 `) ^Fob ; :: thesis: contradiction
hence contradiction by A11, A18, Th20; :: thesis: verum

end;

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

end;

hence ( ( 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) ) by A1; :: thesis: verum