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:
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:
proof
let z be object ; :: 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;
then rng (MergeSequence (p,q)) = {} by ;
then Intersect (rng (MergeSequence (p,q))) = X by SETFAM_1:def 9;
hence z in {X} by ; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {X} or z in Components Y )
p = <*> (bool X) by A2;
then rng (MergeSequence (p,())) = {} by ;
then A5: Intersect (rng (MergeSequence (p,()))) = X by SETFAM_1:def 9;
assume z in {X} ; :: thesis:
then z = X by TARSKI:def 1;
hence z in Components Y by A1, A3, A5; :: thesis: verum
end;