let BL be Boolean Lattice; :: thesis: for A being non empty Subset of BL
for c being Element of BL holds
( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )

let A be non empty Subset of BL; :: thesis: for c being Element of BL holds
( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )

let c be Element of BL; :: thesis: ( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )

hereby :: thesis: ( ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) implies c in SetImp A )
assume c in SetImp A ; :: thesis: ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A )

then consider p, q being Element of BL such that
A1: ( c = p => q & p in A & q in A ) ;
take p = p; :: thesis: ex q being Element of BL st
( c = (p `) "\/" q & p in A & q in A )

take q = q; :: thesis: ( c = (p `) "\/" q & p in A & q in A )
thus ( c = (p `) "\/" q & p in A & q in A ) by ; :: thesis: verum
end;
given p, q being Element of BL such that A2: c = (p `) "\/" q and
A3: ( p in A & q in A ) ; :: thesis: c in SetImp A
c = p => q by ;
hence c in SetImp A by A3; :: thesis: verum