let FMT be non empty FMT_Space_Str ; :: thesis: ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )
A1: ( FMT is Fo_filled implies for A being Subset of FMT holds A c= A ^Fob )

proof

assume A2: FMT is Fo_filled ; :: thesis: for A being Subset of FMT holds A c= A ^Fob
let A be Subset of FMT; :: thesis: A c= A ^Fob
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A ^Fob )
assume A3: x in A ; :: thesis: x in A ^Fob
then reconsider y = x as Element of FMT ;
for W being Subset of FMT st W in U_FMT y holds
W meets A

proof

let W be Subset of FMT; :: thesis: ( W in U_FMT y implies W meets A )
assume W in U_FMT y ; :: thesis: W meets A
then y in W by A2, Def8;
hence W meets A by A3, XBOOLE_0:3; :: thesis: verum

end;

hence x in A ^Fob ; :: thesis: verum

end;

( ( for A being Subset of FMT holds A c= A ^Fob ) implies FMT is Fo_filled )

proof

assume A4: for A being Subset of FMT holds A c= A ^Fob ; :: thesis: FMT is Fo_filled
assume not FMT is Fo_filled ; :: thesis: contradiction
then consider y being Element of FMT, V being Subset of FMT such that
A5: V in U_FMT y and
A6: not y in V by Def8;
A7: V misses {y}

proof

assume V meets {y} ; :: thesis: contradiction
then consider z being set such that
A8: ( z in V & z in {y} ) by XBOOLE_0:3;
thus contradiction by A6, A8, TARSKI:def 1; :: thesis: verum

end;

not {y} c= {y} ^Fob

proof

assume A9: {y} c= {y} ^Fob ; :: thesis: contradiction
y in {y} by TARSKI:def 1;
hence contradiction by A5, A7, A9, Th21; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

hence ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob ) by A1; :: thesis: verum