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

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

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

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

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

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

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

for x being Element of FMT holds

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

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

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

for x being Element of FMT holds

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

proof

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

A2: ( x in (A ^Foi) /\ (B ^Foi) implies x in (A /\ B) ^Foi )

end;A2: ( x in (A ^Foi) /\ (B ^Foi) implies x in (A /\ B) ^Foi )

proof

( x in (A /\ B) ^Foi implies x in (A ^Foi) /\ (B ^Foi) )
assume A3:
x in (A ^Foi) /\ (B ^Foi)
; :: thesis: x in (A /\ B) ^Foi

then x in B ^Foi by XBOOLE_0:def 4;

then A4: ex W2 being Subset of FMT st

( W2 in U_FMT x & W2 c= B ) by Th21;

x in A ^Foi by A3, XBOOLE_0:def 4;

then ex W1 being Subset of FMT st

( W1 in U_FMT x & W1 c= A ) by Th21;

then consider W1, W2 being Subset of FMT such that

A5: ( W1 in U_FMT x & W2 in U_FMT x ) and

A6: W1 c= A and

A7: W2 c= B by A4;

consider W being Subset of FMT such that

A8: W in U_FMT x and

A9: W c= W1 /\ W2 by A1, A5;

W1 /\ W2 c= W2 by XBOOLE_1:17;

then W c= W2 by A9;

then A10: W c= B by A7;

W1 /\ W2 c= W1 by XBOOLE_1:17;

then W c= W1 by A9;

then W c= A by A6;

then W c= A /\ B by A10, XBOOLE_1:19;

hence x in (A /\ B) ^Foi by A8; :: thesis: verum

end;then x in B ^Foi by XBOOLE_0:def 4;

then A4: ex W2 being Subset of FMT st

( W2 in U_FMT x & W2 c= B ) by Th21;

x in A ^Foi by A3, XBOOLE_0:def 4;

then ex W1 being Subset of FMT st

( W1 in U_FMT x & W1 c= A ) by Th21;

then consider W1, W2 being Subset of FMT such that

A5: ( W1 in U_FMT x & W2 in U_FMT x ) and

A6: W1 c= A and

A7: W2 c= B by A4;

consider W being Subset of FMT such that

A8: W in U_FMT x and

A9: W c= W1 /\ W2 by A1, A5;

W1 /\ W2 c= W2 by XBOOLE_1:17;

then W c= W2 by A9;

then A10: W c= B by A7;

W1 /\ W2 c= W1 by XBOOLE_1:17;

then W c= W1 by A9;

then W c= A by A6;

then W c= A /\ B by A10, XBOOLE_1:19;

hence x in (A /\ B) ^Foi by A8; :: thesis: verum

proof

hence
( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi )
by A2; :: thesis: verum
assume A11:
x in (A /\ B) ^Foi
; :: thesis: x in (A ^Foi) /\ (B ^Foi)

(A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) by Th29;

hence x in (A ^Foi) /\ (B ^Foi) by A11; :: thesis: verum

end;(A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) by Th29;

hence x in (A ^Foi) /\ (B ^Foi) by A11; :: 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 ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi )

proof

hence
( ( for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) implies for x being Element of FMT
given x0 being Element of FMT, V1, V2 being Subset of FMT such that A12:
( V1 in U_FMT x0 & 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 ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi

take V1 ; :: thesis: ex B being Subset of FMT st (V1 ^Foi) /\ (B ^Foi) <> (V1 /\ B) ^Foi

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

( x0 in V1 ^Foi & x0 in V2 ^Foi ) by A12;

then x0 in (V1 ^Foi) /\ (V2 ^Foi) by XBOOLE_0:def 4;

hence (V1 ^Foi) /\ (V2 ^Foi) <> (V1 /\ V2) ^Foi by A13, Th21; :: thesis: verum

end;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 ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi

take V1 ; :: thesis: ex B being Subset of FMT st (V1 ^Foi) /\ (B ^Foi) <> (V1 /\ B) ^Foi

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

( x0 in V1 ^Foi & x0 in V2 ^Foi ) by A12;

then x0 in (V1 ^Foi) /\ (V2 ^Foi) by XBOOLE_0:def 4;

hence (V1 ^Foi) /\ (V2 ^Foi) <> (V1 /\ V2) ^Foi by A13, Th21; :: 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 ) ) ; :: thesis: verum