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

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