theorem Th23: :: MEMBER_1:23
for F, G being ext-real-membered set holds (F \/ G) "" = (F "") \/ (G "")