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 ) )
proof
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 )
proof
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 )
proof
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;
( x in (A /\ B) ^Foi implies x in (A ^Foi) /\ (B ^Foi) )
proof
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;
hence ( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi ) by A2; :: thesis: verum
end;
hence (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi 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 ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi )
proof
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;
hence ( ( 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 ) ) ; :: thesis: verum