let X be set ; :: thesis: for Y being empty Subset-Family of X holds Components Y = {X}
let Y be empty Subset-Family of X; :: thesis: Components Y = {X}
consider p being FinSequence of bool X such that
A1: len p = card Y and
A2: rng p = Y and
A3: Components Y = { (Intersect (rng (MergeSequence p,q))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
thus Components Y = {X} :: thesis: verum

proof

thus Components Y c= {X} :: according to XBOOLE_0:def 10 :: thesis: {X} c= Components Y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Components Y or z in {X} )
assume z in Components Y ; :: thesis: z in {X}
then consider q being FinSequence of BOOLEAN such that
A4: z = Intersect (rng (MergeSequence p,q)) and
len q = len p by A3;
p = <*> (bool X) by A2, RELAT_1:64;
then MergeSequence p,q = <*> (bool X) by Th9;
then rng (MergeSequence p,q) = {} by RELAT_1:60;
then Intersect (rng (MergeSequence p,q)) = X by SETFAM_1:def 10;
hence z in {X} by A4, TARSKI:def 1; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {X} or z in Components Y )
assume z in {X} ; :: thesis: z in Components Y
then A5: z = X by TARSKI:def 1;
p = <*> (bool X) by A2, RELAT_1:64;
then MergeSequence p,(<*> BOOLEAN ) = <*> (bool X) by Th9;
then rng (MergeSequence p,(<*> BOOLEAN )) = {} by RELAT_1:60;
then Intersect (rng (MergeSequence p,(<*> BOOLEAN ))) = X by SETFAM_1:def 10;
hence z in Components Y by A1, A3, A5; :: thesis: verum

end;