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