set x = the Element of A;
set B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
reconsider x = the Element of A as Element of BL ;
x => x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
then reconsider B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } as non empty set ;
B = SetImp A ;
hence not SetImp A is empty ; :: thesis: verum