let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B, R being set st R = DisUnion S & A in R & B in R & A <> {} holds
B \ A in R
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for A, B, R being set st R = DisUnion S & A in R & B in R & A <> {} holds
B \ A in R
let A, B, R be set ; :: thesis: ( R = DisUnion S & A in R & B in R & A <> {} implies B \ A in R )
assume that
A1: R = DisUnion S and
A2: ( A in R & B in R & A <> {} ) ; :: thesis: B \ A in R
consider A1 being Subset of X such that
A3: ( A = A1 & ex F being disjoint_valued FinSequence of S st A1 = Union F ) by A1, A2;
consider f1 being disjoint_valued FinSequence of S such that
A4: A1 = Union f1 by A3;
consider B1 being Subset of X such that
A5: ( B = B1 & ex F being disjoint_valued FinSequence of S st B1 = Union F ) by A1, A2;
reconsider R1 = R as non empty set by A2;
defpred S₁[ Nat, object ] means $2 = B1 \ (f1 . $1);
A7: for k being Nat st k in Seg (len f1) holds
ex x being Element of R1 st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len f1) implies ex x being Element of R1 st S₁[k,x] )
assume k in Seg (len f1) ; :: thesis: ex x being Element of R1 st S₁[k,x]
then k in dom f1 by FINSEQ_1:def 3;
then ( f1 . k in rng f1 & rng f1 c= S ) by FUNCT_1:3;
then B1 \ (f1 . k) in R1 by A1, A2, A5, lemma104;
hence ex x being Element of R1 st S₁[k,x] ; :: thesis: verum

end;

consider F being FinSequence of R1 such that
A8: ( dom F = Seg (len f1) & ( for k being Nat st k in Seg (len f1) holds
S₁[k,F . k] ) ) from FINSEQ_1:sch 5(A7);

now :: thesis: for x being object st x in B \ A holds
x in meet (rng F)

let x be object ; :: thesis: ( x in B \ A implies x in meet (rng F) )
assume C9: x in B \ A ; :: thesis: x in meet (rng F)
then ( x in B & not x in A ) by XBOOLE_0:def 5;
then A10: for Y being set holds
( not x in Y or not Y in rng f1 ) by A3, A4, TARSKI:def 4;
B1: for k being Nat st k in Seg (len f1) holds
x in F . k

proof

let k be Nat; :: thesis: ( k in Seg (len f1) implies x in F . k )
assume B2: k in Seg (len f1) ; :: thesis: x in F . k
then B3: F . k = B1 \ (f1 . k) by A8;
k in dom f1 by B2, FINSEQ_1:def 3;
then not x in f1 . k by A10, FUNCT_1:3;
hence x in F . k by A5, C9, B3, XBOOLE_0:def 5; :: thesis: verum

end;

dom f1 <> {} by A2, A3, A4, ZFMISC_1:2, RELAT_1:42;
then consider k being object such that
B4: k in dom f1 by XBOOLE_0:def 1;
reconsider k = k as Nat by B4;
k in Seg (len f1) by B4, FINSEQ_1:def 3;
then B5: rng F <> {} by A8, FUNCT_1:3;

now :: thesis: for Y being set st Y in rng F holds
x in Y

let Y be set ; :: thesis: ( Y in rng F implies x in Y )
assume Y in rng F ; :: thesis: x in Y
then consider k being object such that
B6: ( k in dom F & Y = F . k ) by FUNCT_1:def 3;
reconsider k = k as Nat by B6;
thus x in Y by A8, B6, B1; :: thesis: verum

end;

hence x in meet (rng F) by B5, SETFAM_1:def 1; :: thesis: verum

end;

then B7: B \ A c= meet (rng F) ;

now :: thesis: for x being object st x in meet (rng F) holds
x in B \ A

let x be object ; :: thesis: ( x in meet (rng F) implies x in B \ A )
assume B8: x in meet (rng F) ; :: thesis: x in B \ A
then consider Y being object such that
B10: Y in rng F by SETFAM_1:1, XBOOLE_0:def 1;
consider k being object such that
B11: ( k in dom F & Y = F . k ) by B10, FUNCT_1:def 3;
reconsider k = k as Nat by B11;
x in F . k by B8, B10, B11, SETFAM_1:def 1;
then x in B1 \ (f1 . k) by A8, B11;
then B12: ( x in B1 & not x in f1 . k ) by XBOOLE_0:def 5;

now :: thesis: not x in union (rng f1)

assume x in union (rng f1) ; :: thesis: contradiction
then consider Y being set such that
B13: ( x in Y & Y in rng f1 ) by TARSKI:def 4;
consider k being object such that
B14: ( k in dom f1 & Y = f1 . k ) by B13, FUNCT_1:def 3;
reconsider k = k as Nat by B14;
B15: k in dom F by B14, A8, FINSEQ_1:def 3;
then F . k in rng F by FUNCT_1:3;
then x in F . k by B8, SETFAM_1:def 1;
then x in B1 \ (f1 . k) by B15, A8;
hence contradiction by B13, B14, XBOOLE_0:def 5; :: thesis: verum

end;

hence x in B \ A by A3, A4, A5, B12, XBOOLE_0:def 5; :: thesis: verum

end;

then meet (rng F) c= B \ A ;
then B16: B \ A = meet (rng F) by B7;
defpred S₂[ Nat] means meet (rng (F | $1)) in R;
( meet (rng (F | 0)) in S & S c= R ) by A1, lemma100, SETFAM_1:def 8, SETFAM_1:1;
then C1: S₂[ 0 ] ;
C2: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume C3: S₂[k] ; :: thesis: S₂[k + 1]

per cases ( k + 1 <= len F or k + 1 > len F ) ;

suppose C4: k + 1 <= len F ; :: thesis: S₂[k + 1]

F | k = (F | (k + 1)) | k by FINSEQ_1:82, NAT_1:11;
then F | (k + 1) = (F | k) ^ <*((F | (k + 1)) . (k + 1))*> by C4, FINSEQ_1:59, FINSEQ_3:55;
then C6: rng (F | (k + 1)) = (rng (F | k)) \/ (rng <*((F | (k + 1)) . (k + 1))*>) by FINSEQ_1:31
.= (rng (F | k)) \/ {((F | (k + 1)) . (k + 1))} by FINSEQ_1:38
.= (rng (F | k)) \/ {(F . (k + 1))} by FINSEQ_3:112 ;
k + 1 in dom F by C4, FINSEQ_3:25, NAT_1:11;
then C9: ( F . (k + 1) in rng F & rng F c= R1 ) by FUNCT_1:3;
then C7: F . (k + 1) in R ;

per cases ( rng (F | k) <> {} or rng (F | k) = {} ) ;

suppose rng (F | k) <> {} ; :: thesis: S₂[k + 1]

then C8: meet (rng (F | (k + 1))) = (meet (rng (F | k))) /\ (meet {(F . (k + 1))}) by C6, SETFAM_1:9
.= (meet (rng (F | k))) /\ (F . (k + 1)) by SETFAM_1:10 ;
R is cap-closed by A1, lemma101;
hence meet (rng (F | (k + 1))) in R by C3, C9, C8; :: thesis: verum

end;

suppose rng (F | k) = {} ; :: thesis: S₂[k + 1]

hence meet (rng (F | (k + 1))) in R by C6, C7, SETFAM_1:10; :: thesis: verum

end;

end;

end;

suppose k + 1 > len F ; :: thesis: S₂[k + 1]

then ( F | k = F & F | (k + 1) = F ) by FINSEQ_1:58, NAT_1:13;
hence meet (rng (F | (k + 1))) in R by C3; :: thesis: verum

end;

end;

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(C1, C2);
then S₂[ len F] ;
hence B \ A in R by B16, FINSEQ_1:58; :: thesis: verum