let X1, X2 be Subset of fin_RelStr ; :: thesis: ( ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in X1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X1 & H2 in X1 holds
( union_of H1,H2 in X1 & sum_of H1,H2 in X1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
X1 c= M ) & ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in X2 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X2 & H2 in X2 holds
( union_of H1,H2 in X2 & sum_of H1,H2 in X2 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
X2 c= M ) implies X1 = X2 )
assume that
A25: for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in X1 and
A26: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X1 & H2 in X1 holds
( union_of H1,H2 in X1 & sum_of H1,H2 in X1 ) and
A27: for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
X1 c= M and
A28: for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in X2 and
A29: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X2 & H2 in X2 holds
( union_of H1,H2 in X2 & sum_of H1,H2 in X2 ) and
A30: for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
X2 c= M ; :: thesis: X1 = X2
( X1 c= X2 & X2 c= X1 ) by A25, A26, A27, A28, A29, A30;
hence X1 = X2 by XBOOLE_0:def 10; :: thesis: verum