theorem Th12: :: FUNCOP_1:12

for A, B being set
for x being object holds (A --> x) | B = (A /\ B) --> x