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

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