per cases
( x in dom F or not x in dom F )
;

end;

suppose A1:
x in dom F
; :: thesis: F . x is Subset-Family of X

A2:
rng F c= bool A
by RELAT_1:def 19;

A3: bool A c= bool (bool X) by ZFMISC_1:67;

F . x in rng F by A1, FUNCT_1:def 3;

then F . x in bool A by A2;

hence F . x is Subset-Family of X by A3; :: thesis: verum

end;A3: bool A c= bool (bool X) by ZFMISC_1:67;

F . x in rng F by A1, FUNCT_1:def 3;

then F . x in bool A by A2;

hence F . x is Subset-Family of X by A3; :: thesis: verum