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 A1, FILTER_0:42; :: 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 A2, FILTER_0:42;
hence c in SetImp A by A3; :: thesis: verum