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 )

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

proof

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

end;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

not {y} c= {y} ^Fob
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;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

proof

hence
contradiction
by A2; :: thesis: verum
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;assume {y} c= {y} ^Fob ; :: thesis: contradiction

hence contradiction by A3, A5, A6, Th20; :: thesis: verum

proof

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

end;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

hence
x in A ^Fob
; :: thesis: verum
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;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