the carrier of BL c= the carrier of BL
;

then reconsider F = the carrier of BL as non empty Subset of BL ;

take F ; :: thesis: for a, b being Element of BL st a in F & b in F holds

( a "/\" b in F & a ` in F )

thus for a, b being Element of BL st a in F & b in F holds

( a "/\" b in F & a ` in F ) ; :: thesis: verum

then reconsider F = the carrier of BL as non empty Subset of BL ;

take F ; :: thesis: for a, b being Element of BL st a in F & b in F holds

( a "/\" b in F & a ` in F )

thus for a, b being Element of BL st a in F & b in F holds

( a "/\" b in F & a ` in F ) ; :: thesis: verum