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 ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
let x be Element of FMT; :: thesis: for A being Subset of FMT holds
( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
let A be Subset of FMT; :: thesis: ( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
thus ( x in A ^Fodelta implies for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ) :: thesis: ( ( for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ) implies x in A ^Fodelta )

proof

assume x in A ^Fodelta ; :: thesis: for W being Subset of FMT st W in U_FMT x holds
( W meets A & 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 & W meets A ` ) ) ) ;
hence for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ; :: thesis: verum

end;

assume for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ; :: thesis: x in A ^Fodelta
hence x in A ^Fodelta ; :: thesis: verum