let FMT be non empty FMT_Space_Str ; :: thesis: for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob )
let A, B be Subset of FMT; :: thesis: ( FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) implies (A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob ) )
assume A1: FMT is Fo_filled ; :: thesis: ( ex x being Element of FMT st not {x} in U_FMT x or (A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob ) )
assume A2: for x being Element of FMT holds {x} in U_FMT x ; :: thesis: (A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob )
A3: for C being Subset of FMT holds C ^Fob c= C

proof

let C be Subset of FMT; :: thesis: C ^Fob c= C
for y being Element of FMT st y in C ^Fob holds
y in C

proof

let y be Element of FMT; :: thesis: ( y in C ^Fob implies y in C )
assume A4: y in C ^Fob ; :: thesis: y in C
{y} in U_FMT y by A2;
then {y} meets C by A4, Th21;
then ex z being set st
( z in {y} & z in C ) by XBOOLE_0:3;
hence y in C by TARSKI:def 1; :: thesis: verum

end;

hence C ^Fob c= C by SUBSET_1:7; :: thesis: verum

end;

A5: for C being Subset of FMT holds C ^Fob = C

proof

let C be Subset of FMT; :: thesis: C ^Fob = C
( C c= C ^Fob & C ^Fob c= C ) by A1, A3, Th36;
hence C ^Fob = C by XBOOLE_0:def 10; :: thesis: verum

end;

then ( (A /\ B) ^Fob = A /\ B & A ^Fob = A ) ;
hence (A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob ) by A5; :: thesis: verum