let X1, X2 be Subset of fin_RelStr; :: thesis: ( ( for R being strict RelStr st the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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
A31: X2 c= X1 by A25, A26, A30;
X1 c= X2 by A27, A28, A29;
hence X1 = X2 by A31, XBOOLE_0:def 10; :: thesis: verum