theorem :: FINTOPO2:32
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) holds
(A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)