consider a being Element of I;
set X = { |.(A . i).| where i is Element of I : verum } ;
( |.(A . a).| in { |.(A . i).| where i is Element of I : verum } & ex x being set st x in |.(A . a).| ) by XBOOLE_0:def 1;
hence not |.A.| is empty by TARSKI:def 4; :: thesis: verum