theorem Th12: :: FINTOPO6:13

for FT being non empty RelStr
for X9 being non empty SubSpace of FT
for A being Subset of FT
for A1 being Subset of X9 st A = A1 holds
A1 ^b = (A ^b) /\ ([#] X9)