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, Th21;
then W1 /\ (A \/ B) <> {} by XBOOLE_0:def 7;
then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23;
then ( W1 /\ A <> {} or W1 /\ B <> {} ) ;
hence ( W1 meets A or W1 meets B ) by XBOOLE_0:def 7; :: 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, XBOOLE_1:1;
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, XBOOLE_1:1;
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 <> {} ) by XBOOLE_0:def 7;
then ex z1, z2 being Element of FMT st
( z1 in W /\ A or z2 in W /\ B ) by SUBSET_1:10;
hence ( V1 meets A or V2 meets B ) by A8, A9, XBOOLE_0:def 7; :: 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 Th27;
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:8; :: 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, Th21; :: 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:32;
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, Th21; :: 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