let X be set ; :: thesis: for Y being finite Subset-Family of X
for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B

let Y be finite Subset-Family of X; :: thesis: for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B

let A, B be set ; :: thesis: ( A in Components Y & B in Components Y & A <> B implies A misses B )
assume that
A1: A in Components Y and
A2: B in Components Y and
A3: A <> B ; :: thesis: A misses B
assume A /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider z being object such that
A4: z in A /\ B by XBOOLE_0:def 1;
A5: z in B by ;
A6: z in A by ;
consider p being FinSequence of bool X such that
len p = card Y and
rng p = Y and
A7: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
consider q1 being FinSequence of BOOLEAN such that
A8: A = Intersect (rng (MergeSequence (p,q1))) and
len q1 = len p by A1, A7;
consider q2 being FinSequence of BOOLEAN such that
A9: B = Intersect (rng (MergeSequence (p,q2))) and
len q2 = len p by A2, A7;
A10: len (MergeSequence (p,q1)) = len p by Def1;
then A11: dom (MergeSequence (p,q1)) = Seg (len p) by FINSEQ_1:def 3;
A12: now :: thesis: for i being Nat st i in dom (MergeSequence (p,q1)) holds
(MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i
let i be Nat; :: thesis: ( i in dom (MergeSequence (p,q1)) implies (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1 )
assume A13: i in dom (MergeSequence (p,q1)) ; :: thesis: (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1
then A14: i in dom p by ;
(MergeSequence (p,q1)) . i in rng (MergeSequence (p,q1)) by ;
then A15: z in (MergeSequence (p,q1)) . i by ;
i in dom (MergeSequence (p,q2)) by ;
then (MergeSequence (p,q2)) . i in rng (MergeSequence (p,q2)) by FUNCT_1:def 3;
then A16: z in (MergeSequence (p,q2)) . i by ;
per cases ( q1 . i = TRUE or q1 . i = FALSE ) by XBOOLEAN:def 3;
suppose q1 . i = TRUE ; :: thesis: (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1
then A17: (MergeSequence (p,q1)) . i = p . i by Th2;
q2 . i = TRUE
proof
assume not q2 . i = TRUE ; :: thesis: contradiction
then (MergeSequence (p,q2)) . i = X \ (p . i) by ;
hence contradiction by A15, A16, A17, XBOOLE_0:def 5; :: thesis: verum
end;
hence (MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i by ; :: thesis: verum
end;
suppose q1 . i = FALSE ; :: thesis: (MergeSequence (p,q1)) . b1 = (MergeSequence (p,q2)) . b1
then A18: (MergeSequence (p,q1)) . i = X \ (p . i) by ;
q2 . i = FALSE hence (MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i by ; :: thesis: verum
end;
end;
end;
len (MergeSequence (p,q2)) = len p by Def1;
hence contradiction by A3, A8, A9, A10, A12, FINSEQ_2:9; :: thesis: verum