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 object ; :: 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 and
A5: V c= A by A3, Th21;
y in V by A2, A4;
hence x in A by A5; :: thesis: verum
end;
( ( for A being Subset of FMT holds A ^Foi c= A ) implies FMT is Fo_filled )
proof
assume A6: 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
A7: V in U_FMT y and
A8: not y in V ;
y in V ^Foi by A7;
then not V ^Foi c= V by A8;
hence contradiction by A6; :: thesis: verum
end;
hence ( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A ) by A1; :: thesis: verum