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 )

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

proof

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

proof

hence
( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )
by A1; :: thesis: verum
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;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