let FMT be non empty FMT_Space_Str ; :: thesis: for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

let x be Element of FMT; :: thesis: for A being Subset of FMT holds

( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

let A be Subset of FMT; :: thesis: ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

thus ( x in A ^Fob implies for W being Subset of FMT st W in U_FMT x holds

W meets A ) :: thesis: ( ( for W being Subset of FMT st W in U_FMT x holds

W meets A ) implies x in A ^Fob )

W meets A ; :: thesis: x in A ^Fob

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

for A being Subset of FMT holds

( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

let x be Element of FMT; :: thesis: for A being Subset of FMT holds

( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

let A be Subset of FMT; :: thesis: ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

thus ( x in A ^Fob implies for W being Subset of FMT st W in U_FMT x holds

W meets A ) :: thesis: ( ( for W being Subset of FMT st W in U_FMT x holds

W meets A ) implies x in A ^Fob )

proof

assume
for W being Subset of FMT st W in U_FMT x holds
assume
x in A ^Fob
; :: thesis: for W being Subset of FMT st W in U_FMT x holds

W meets A

then ex y being Element of FMT st

( y = x & ( for W being Subset of FMT st W in U_FMT y holds

W meets A ) ) ;

hence for W being Subset of FMT st W in U_FMT x holds

W meets A ; :: thesis: verum

end;W meets A

then ex y being Element of FMT st

( y = x & ( for W being Subset of FMT st W in U_FMT y holds

W meets A ) ) ;

hence for W being Subset of FMT st W in U_FMT x holds

W meets A ; :: thesis: verum

W meets A ; :: thesis: x in A ^Fob

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