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

proof

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 x in (A ^Foi ) /\ (B ^Foi ) ; :: thesis: x in (A /\ B) ^Foi
then ( x in A ^Foi & x in B ^Foi ) by XBOOLE_0:def 4;
then ( ex W1 being Subset of FMT st
( W1 in U_FMT x & W1 c= A ) & ex W2 being Subset of FMT st
( W2 in U_FMT x & W2 c= B ) ) by Th22;
then consider W1, W2 being Subset of FMT such that
A3: ( W1 in U_FMT x & W2 in U_FMT x ) and
A4: ( W1 c= A & W2 c= B ) ;
consider W being Subset of FMT such that
A5: W in U_FMT x and
A6: W c= W1 /\ W2 by A1, A3;
( W1 /\ W2 c= W1 & W1 /\ W2 c= W2 ) by XBOOLE_1:17;
then ( W c= W1 & W c= W2 ) by A6, XBOOLE_1:1;
then ( W in U_FMT x & W c= A & W c= B ) by A4, A5, XBOOLE_1:1;
then ( W in U_FMT x & W c= A /\ B ) by XBOOLE_1:19;
hence x in (A /\ B) ^Foi ; :: thesis: verum

end;

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

proof

assume A7: x in (A /\ B) ^Foi ; :: thesis: x in (A ^Foi ) /\ (B ^Foi )
(A /\ B) ^Foi c= (A ^Foi ) /\ (B ^Foi ) by Th30;
hence x in (A ^Foi ) /\ (B ^Foi ) by A7; :: 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:8; :: thesis: verum

end;

thus verum ; :: thesis: verum

end;

thus ( ( 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

proof

( 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 A8: ( V1 in U_FMT x0 & V2 in U_FMT x0 ) and
A9: 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
( x0 in V1 ^Foi & x0 in V2 ^Foi ) by A8;
then A10: ( x0 in (V1 ^Foi ) /\ (V2 ^Foi ) & not x0 in (V1 /\ V2) ^Foi ) by A9, Th22, XBOOLE_0:def 4;
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
thus (V1 ^Foi ) /\ (V2 ^Foi ) <> (V1 /\ V2) ^Foi by A10; :: 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

end;