theorem :: FINANCE3:17

for A1 being SetSequence of {1,2,3,4}
for MyOmega being set st MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1 = {3,4} holds
Intersection A1 in MyOmega by ENUMSET1:def 2;