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, Th20;
then ex z being object 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 ; :: thesis: verum

end;

A5: for C being Subset of FMT holds C ^Fob = C by A1, A3, Th35;
then ( (A /\ B) ^Fob = A /\ B & A ^Fob = A ) ;
hence (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) by A5; :: thesis: verum