set Y = fin_RelStr_sp ;
let X be set ; :: thesis:
assume A1: X in fin_RelStr_sp ; :: thesis:
assume A2: X is not non empty trivial strict RelStr ; :: thesis:
deffunc H₁( set , set ) -> set = $2 \/ { x where x is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in $2 & R2 in $2 & ( x = union_of R1,R2 or x = sum_of R1,R2 ) ) } ;
consider f being Function such that
A3: dom f = NAT and
A4: f . 0 = { x where x is Element of fin_RelStr_sp : x is trivial RelStr } and
A5: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
A6: for i being Nat holds f . i c= f . (i + 1)

proof

let i be Nat; :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in f . i ; :: thesis:
f . (i + 1) = (f . i) \/ { b where b is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . i & R2 in f . i & ( b = union_of R1,R2 or b = sum_of R1,R2 ) ) } by A5;
hence x in f . (i + 1) by A7, XBOOLE_0:def 3; :: thesis:

end;

A8: for i, j being Element of NAT st i <= j holds
f . i c= f . j

proof

let i, j be Element of NAT ; :: thesis:
assume i <= j ; :: thesis:
then consider k being Nat such that
A9: j = i + k by NAT_1:10;
defpred S₁[ Nat] means f . i c= f . (i + $1);
A10: S₁[ 0 ] ;
A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A12: S₁[k] ; :: thesis:
f . (i + k) c= f . ((i + k) + 1) by A6;
hence S₁[k + 1] by A12, XBOOLE_1:1; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A11);
hence f . i c= f . j by A9; :: thesis:

end;

A13: Union f c= fin_RelStr_sp

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in Union f ; :: thesis:
then consider x being set such that
A14: x in dom f and
A15: y in f . x by CARD_5:10;
defpred S₁[ Nat] means f . $1 c= fin_RelStr_sp ;
A16: S₁[ 0 ]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in f . 0 ; :: thesis:
then ex a being Element of fin_RelStr_sp st
( y = a & a is trivial RelStr ) by A4;
hence y in fin_RelStr_sp ; :: thesis:

end;

A17: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A18: S₁[k] ; :: thesis:
A19: f . (k + 1) = (f . k) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } by A5;
{ a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } c= fin_RelStr_sp

proof

set S = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } ;
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } ; :: thesis:
then consider a being Element of fin_RelStr_sp such that
A20: ( x = a & ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) ) ;
thus x in fin_RelStr_sp by A20; :: thesis:

end;

hence S₁[k + 1] by A18, A19, XBOOLE_1:8; :: thesis:

end;

reconsider x = x as Element of NAT by A3, A14;
for k being Nat holds S₁[k] from NAT_1:sch 2(A16, A17);
then f . x c= fin_RelStr_sp ;
hence y in fin_RelStr_sp by A15; :: thesis:

end;

then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
A21: 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

proof

let R be strict RelStr ; :: thesis:
assume that
A22: ( not the carrier of R is empty & the carrier of R is trivial ) and
A23: the carrier of R in FinSETS ; :: thesis:
A24: R is Element of fin_RelStr_sp by A22, A23, Def5;
R is trivial RelStr by A22;
then A25: R in f . 0 by A4, A24;
f . 0 c= M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in f . 0 ; :: thesis:
hence x in M by A3, CARD_5:10; :: thesis:

end;

hence R in M by A25; :: thesis:

end;

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 )

proof

let H1, H2 be strict RelStr ; :: thesis:
assume that
A26: the carrier of H1 misses the carrier of H2 and
A27: H1 in M and
A28: H2 in M ; :: thesis:
consider x1 being set such that
A29: x1 in dom f and
A30: H1 in f . x1 by A27, CARD_5:10;
consider x2 being set such that
A31: x2 in dom f and
A32: H2 in f . x2 by A28, CARD_5:10;
reconsider x1 = x1, x2 = x2 as Element of NAT by A3, A29, A31;
A33: max x1,x2 in NAT by ORDINAL1:def 13;
A34: (max x1,x2) + 1 in dom f by A3;
A35: f . x1 c= f . (max x1,x2) by A8, A33, XXREAL_0:25;
A36: f . x2 c= f . (max x1,x2) by A8, A33, XXREAL_0:25;
set W = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max x1,x2) & R2 in f . (max x1,x2) & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } ;
A37: f . ((max x1,x2) + 1) = (f . (max x1,x2)) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max x1,x2) & R2 in f . (max x1,x2) & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } by A5;
union_of H1,H2 in fin_RelStr_sp by A13, A26, A27, A28, Def5;
then union_of H1,H2 in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max x1,x2) & R2 in f . (max x1,x2) & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } by A26, A30, A32, A35, A36;
then A38: union_of H1,H2 in f . ((max x1,x2) + 1) by A37, XBOOLE_0:def 3;
sum_of H1,H2 in fin_RelStr_sp by A13, A26, A27, A28, Def5;
then sum_of H1,H2 in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max x1,x2) & R2 in f . (max x1,x2) & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } by A26, A30, A32, A35, A36;
then sum_of H1,H2 in f . ((max x1,x2) + 1) by A37, XBOOLE_0:def 3;
hence ( union_of H1,H2 in M & sum_of H1,H2 in M ) by A34, A38, CARD_5:10; :: thesis:

end;

then A39: fin_RelStr_sp c= M by A21, Def5;
then A40: Union f = fin_RelStr_sp by A13, XBOOLE_0:def 10;
ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) )

proof

consider y being set such that
A41: y in dom f and
A42: X in f . y by A1, A39, CARD_5:10;
defpred S₁[ Nat] means ( X in f . $1 implies ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) );
A43: S₁[ 0 ]

proof

assume X in f . 0 ; :: thesis:
then consider a being Element of fin_RelStr_sp such that
A44: X = a and
A45: a is trivial RelStr by A4;
thus ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) by A2, A44, A45, Th4; :: thesis:

end;

A46: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let n be Nat; :: thesis:
assume A47: S₁[n] ; :: thesis:
set W = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } ;
assume A48: X in f . (n + 1) ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A49: f . (n + 1) = (f . n) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } by A5;

per cases by A48, A49, XBOOLE_0:def 3;

suppose X in f . n ; :: thesis:

hence ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) by A47; :: thesis:

end;

suppose X in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) } ; :: thesis:

then consider a being Element of fin_RelStr_sp such that
A50: a = X and
A51: ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of R1,R2 or a = sum_of R1,R2 ) ) ;
consider R1, R2 being strict RelStr such that
A52: the carrier of R1 misses the carrier of R2 and
A53: ( R1 in f . n & R2 in f . n & ( X = union_of R1,R2 or X = sum_of R1,R2 ) ) by A50, A51;
( R1 in fin_RelStr_sp & R2 in fin_RelStr_sp ) by A3, A40, A53, CARD_5:10;
hence ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) by A52, A53; :: thesis:

end;

A54: y is Nat by A3, A41;
for n being Nat holds S₁[n] from NAT_1:sch 2(A43, A46);
hence ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) by A42, A54; :: thesis:

end;

hence ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) ; :: thesis: