let X be set ; :: thesis: BoolePoset X,(BoolePoset 1) |^ X are_isomorphic
consider f being Function of (BoolePoset X),((BoolePoset 1) |^ 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