theorem :: TOPGEN_1:7

for T being TopSpace
for F, G being Subset-Family of T holds Fr (F \/ G) = (Fr F) \/ (Fr G)