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