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

proof

assume A2: FMT is Fo_filled ; :: thesis: for A being Subset of FMT holds A ^Foi c= A
let A be Subset of FMT; :: thesis: A ^Foi c= A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^Foi or x in A )
assume A3: x in A ^Foi ; :: thesis: x in A
then reconsider y = x as Element of FMT ;
consider V being Subset of FMT such that
A4: ( V in U_FMT y & V c= A ) by A3, Th22;
( y in V & V c= A ) by A2, A4, Def8;
hence x in A ; :: thesis: verum

end;

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

proof

assume A5: for A being Subset of FMT holds A ^Foi c= A ; :: 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
A6: V in U_FMT y and
A7: not y in V by Def8;
y in V ^Foi by A6;
then not V ^Foi c= V by A7;
hence contradiction by A5; :: thesis: verum

end;

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