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 ) )

A3: ( p in A & q in A ) ; :: thesis: c in SetImp A

c = p => q by A2, FILTER_0:42;

hence c in SetImp A by A3; :: thesis: verum

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 )

given p, q being Element of BL such that A2:
c = (p `) "\/" q
and ( 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 A1, FILTER_0:42; :: thesis: verum

end;( 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 A1, FILTER_0:42; :: thesis: verum

A3: ( p in A & q in A ) ; :: thesis: c in SetImp A

c = p => q by A2, FILTER_0:42;

hence c in SetImp A by A3; :: thesis: verum