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

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

proof

hence
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL
; :: thesis: verum
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;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