reconsider Y = X as non empty Subset of (product (I --> L)) ;
set f = the Element of Y;
reconsider f = the Element of Y as Function ;
f . i in pi (X,i) by CARD_3:def 6;
hence not pi (X,i) is empty ; :: thesis: verum