theorem Lm700000: :: FINANCE3:15

for A1 being SetSequence of {1,2,3,4} st ( for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) & rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} & not Intersection A1 = {} & not Intersection A1 = {1,2} & not Intersection A1 = {3,4} holds
Intersection A1 = {1,2,3,4}