let X be set ; :: thesis: BoolePoset X,(BoolePoset {0}) |^ X are_isomorphic
consider f being Function of (BoolePoset X),((BoolePoset {0}) |^ X) such that
A1: f is isomorphic and
for Y being Subset of X holds f . Y = chi (Y,X) by Th17;
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
thus f is isomorphic by A1; :: thesis: verum