set B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } c= the carrier of BL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } or x in the carrier of BL )
assume x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; :: thesis: x in the carrier of BL
then ex p, q being Element of BL st
( x = p => q & p in A & q in A ) ;
hence x in the carrier of BL ; :: thesis: verum

end;

hence { (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL ; :: thesis: verum