set X = { |.(A . i).| where i is Element of I : verum } ;
consider a being Element of I;
A1: |.(A . a).| in { |.(A . i).| where i is Element of I : verum } ;
consider x being set such that
A2: x in |.(A . a).| by XBOOLE_0:def 1;
thus not |.A.| is empty by A1, A2, TARSKI:def 4; :: thesis: verum