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: ( ( for A being Subset of FMT holds A c= A ^Fob ) implies FMT is Fo_filled )

proof

assume A2: 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
A3: V in U_FMT y and
A4: not y in V ;
A5: V misses {y}

proof

assume V meets {y} ; :: thesis: contradiction
then ex z being object st
( z in V & z in {y} ) by XBOOLE_0:3;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum

end;

not {y} c= {y} ^Fob

proof

A6: y in {y} by TARSKI:def 1;
assume {y} c= {y} ^Fob ; :: thesis: contradiction
hence contradiction by A3, A5, A6, Th20; :: thesis: verum

end;

hence contradiction by A2; :: thesis: verum

end;

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

proof

assume A7: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A ^Fob )
assume A8: 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 A7;
hence W meets A by A8, XBOOLE_0:3; :: thesis: verum

end;

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

end;

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