let FMT be non empty FMT_Space_Str ; :: thesis:
let x be Element of ; :: thesis:
let A be Subset of ; :: thesis:
thus ( x in A ^Fodelta implies for W being Subset of st W in U_FMT x holds
( W meets A & W meets A ` ) ) :: thesis:

assume x in A ^Fodelta ; :: thesis:
then ex y being Element of st
( y = x & ( for W being Subset of st W in U_FMT y holds
( W meets A & W meets A ` ) ) ) ;
hence for W being Subset of st W in U_FMT x holds
( W meets A & W meets A ` ) ; :: thesis:

end;