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 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 Th5, RELAT_1:38;
then Intersect (rng (MergeSequence (p,q))) = X by SETFAM_1:def 9;
hence z in {X} by A4, TARSKI:def 1; :: 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,(<*> BOOLEAN))) = {} by Th5, RELAT_1:38;
then A5: Intersect (rng (MergeSequence (p,(<*> BOOLEAN)))) = X by SETFAM_1:def 9;
assume z in {X} ; :: thesis: z in Components Y
then z = X by TARSKI:def 1;
hence z in Components Y by A1, A3, A5; :: thesis: verum
end;