let A1 be SetSequence of {1,2,3,4}; :: thesis: ( ex n being Nat st A1 . n = {} implies Intersection A1 = {} )
given n being Nat such that AB: A1 . n = {} ; :: thesis: Intersection A1 = {}
assume Intersection A1 <> {} ; :: thesis: contradiction
then consider x being object such that
AA: x in Intersection A1 by XBOOLE_0:def 1;
thus contradiction by AB, PROB_1:13, AA; :: thesis: verum