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

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

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;proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {X} or z in Components Y )
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;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

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