let X be set ; :: thesis: for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z

let Y, Z be finite Subset-Family of X; :: thesis: ( Z c= Y implies Components Y is_finer_than Components Z )
assume A1: Z c= Y ; :: thesis:
now :: thesis: for V being set st V in Components Y holds
ex W being set st
( W in Components Z & V c= W )
let V be set ; :: thesis: ( V in Components Y implies ex W being set st
( W in Components Z & V c= W ) )

consider p being FinSequence of bool X such that
A2: len p = card Y and
A3: rng p = Y and
A4: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
consider p1 being FinSequence of bool X such that
len p1 = card Z and
A5: rng p1 = Z and
A6: Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by Def2;
A7: p1 is FinSequence of rng p by ;
assume V in Components Y ; :: thesis: ex W being set st
( W in Components Z & V c= W )

then consider q being FinSequence of BOOLEAN such that
A8: V = Intersect (rng (MergeSequence (p,q))) and
A9: len q = len p by A4;
dom p = dom q by ;
then A10: q is Function of (dom p),BOOLEAN by FINSEQ_2:26;
A11: p is one-to-one by ;
then A12: rng p1 c= dom (p ") by ;
rng (p ") = dom p by
.= dom q by ;
then A13: rng ((p ") * p1) c= dom q by RELAT_1:26;
p is Function of (dom p),(rng p) by FUNCT_2:1;
then p " is Function of (rng p),(dom p) by ;
then (p ") * p1 is FinSequence of dom p by ;
then q * ((p ") * p1) is FinSequence of BOOLEAN by ;
then reconsider q1 = (q * (p ")) * p1 as FinSequence of BOOLEAN by RELAT_1:36;
reconsider W = Intersect (rng (MergeSequence (p1,q1))) as set ;
take W = W; :: thesis: ( W in Components Z & V c= W )
dom q1 = dom (q * ((p ") * p1)) by RELAT_1:36
.= dom ((p ") * p1) by
.= dom p1 by ;
then len q1 = len p1 by FINSEQ_3:29;
hence W in Components Z by A6; :: thesis: V c= W
rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p,q))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p,q)) )
assume z in rng (MergeSequence (p1,q1)) ; :: thesis: z in rng (MergeSequence (p,q))
then consider i being Nat such that
A14: i in dom (MergeSequence (p1,q1)) and
A15: (MergeSequence (p1,q1)) . i = z by FINSEQ_2:10;
A16: i in dom p1 by ;
then A17: i in dom ((p ") * p1) by ;
then ((p ") * p1) . i in rng ((p ") * p1) by FUNCT_1:def 3;
then A18: ((p ") * p1) . i in rng (p ") by FUNCT_1:14;
then A19: ((p ") * p1) . i in dom p by ;
then reconsider j = ((p ") * p1) . i as Element of NAT ;
A20: q . j = (q * ((p ") * p1)) . i by
.= q1 . i by RELAT_1:36 ;
A21: p1 is Function of (dom p1),(rng p) by ;
A22: j in dom p by ;
A23: now :: thesis: (MergeSequence (p,q)) . j = z
per cases ( q . j = TRUE or q . j = FALSE ) by XBOOLEAN:def 3;
suppose A24: q . j = TRUE ; :: thesis: (MergeSequence (p,q)) . j = z
hence (MergeSequence (p,q)) . j = p . j by Th2
.= (p * ((p ") * p1)) . i by
.= ((p * (p ")) * p1) . i by RELAT_1:36
.= ((id (rng p)) * p1) . i by
.= p1 . i by
.= z by A15, A20, A24, Th2 ;
:: thesis: verum
end;
suppose A25: q . j = FALSE ; :: thesis: (MergeSequence (p,q)) . j = z
hence (MergeSequence (p,q)) . j = X \ (p . j) by
.= X \ ((p * ((p ") * p1)) . i) by
.= X \ (((p * (p ")) * p1) . i) by RELAT_1:36
.= X \ (((id (rng p)) * p1) . i) by
.= X \ (p1 . i) by
.= z by A15, A16, A20, A25, Th3 ;
:: thesis: verum
end;
end;
end;
j in dom (MergeSequence (p,q)) by ;
hence z in rng (MergeSequence (p,q)) by ; :: thesis: verum
end;
hence V c= W by ; :: thesis: verum
end;
hence Components Y is_finer_than Components Z by SETFAM_1:def 2; :: thesis: verum