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

then ( (A /\ B) ^Fob = A /\ B & A ^Fob = A ) ;

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

(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

A5:
for C being Subset of FMT holds C ^Fob = C
by A1, A3, Th35;
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

end;for y being Element of FMT st y in C ^Fob holds

y in C

proof

hence
C ^Fob c= C
; :: thesis: verum
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;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

then ( (A /\ B) ^Fob = A /\ B & A ^Fob = A ) ;

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