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 ^Fob implies for W being Subset of st W in U_FMT x holds
W meets A ) :: thesis:

assume x in A ^Fob ; :: 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 ) ) ;
hence for W being Subset of st W in U_FMT x holds
W meets A ; :: thesis:

end;