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) ) ) } ;
set Y = fin_RelStr_sp ;
let X be set ; :: thesis: ( not X in fin_RelStr_sp or X is 1 -element strict RelStr or 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) ) ) )
assume A1: X in fin_RelStr_sp ; :: thesis: ( X is 1 -element strict RelStr or 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) ) ) )
consider f being Function such that
A2: dom f = NAT and
A3: f . 0 = { x where x is Element of fin_RelStr_sp : x is trivial RelStr } and
A4: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
A5: Union f c= fin_RelStr_sp

proof

defpred S₁[ Nat] means f . $1 c= fin_RelStr_sp ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union f or y in fin_RelStr_sp )
assume y in Union f ; :: thesis: y in fin_RelStr_sp
then consider x being object such that
A6: x in dom f and
A7: y in f . x by CARD_5:2;
reconsider x = x as Element of NAT by A2, A6;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
A10: { 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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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) ) ) } or x in fin_RelStr_sp )
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) ) ) } ;
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: x in fin_RelStr_sp
then ex a being Element of fin_RelStr_sp st
( 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) ) ) ) ;
hence x in fin_RelStr_sp ; :: thesis: verum

end;

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 A4;
hence S₁[k + 1] by A9, A10, XBOOLE_1:8; :: thesis: verum

end;

A11: S₁[ 0 ]

proof

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A8);
then f . x c= fin_RelStr_sp ;
hence y in fin_RelStr_sp by A7; :: thesis: verum

end;

then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
A12: for i being Nat holds f . i c= f . (i + 1)

proof

let i be Nat; :: thesis: f . i c= f . (i + 1)
A13: 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 A4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . i or x in f . (i + 1) )
assume x in f . i ; :: thesis: x in f . (i + 1)
hence x in f . (i + 1) by A13, XBOOLE_0:def 3; :: thesis: verum

end;

A14: 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: ( i <= j implies f . i c= f . j )
defpred S₁[ Nat] means f . i c= f . (i + $1);
assume i <= j ; :: thesis: f . i c= f . j
then A15: ex k being Nat st j = i + k by NAT_1:10;
A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

A18: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A18, A16);
hence f . i c= f . j by A15; :: thesis: verum

end;

A19: 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: ( the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M implies ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) )
assume that
A20: the carrier of H1 misses the carrier of H2 and
A21: H1 in M and
A22: H2 in M ; :: thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )
consider x2 being object such that
A23: x2 in dom f and
A24: H2 in f . x2 by A22, CARD_5:2;
consider x1 being object such that
A25: x1 in dom f and
A26: H1 in f . x1 by A21, CARD_5:2;
reconsider x1 = x1, x2 = x2 as Element of NAT by A2, A25, A23;
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) ) ) } ;
A27: 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 A4;
A28: f . x1 c= f . (max (x1,x2)) by A14, XXREAL_0:25;
A29: f . x2 c= f . (max (x1,x2)) by A14, XXREAL_0:25;
sum_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, 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 A20, A26, A24, A28, A29;
then A30: sum_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def 3;
union_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, 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 A20, A26, A24, A28, A29;
then union_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def 3;
hence ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) by A2, A30, CARD_5:2; :: thesis: verum

end;

for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M

proof

A31: f . 0 c= M by A2, CARD_5:2;
let R be strict RelStr ; :: thesis: ( the carrier of R is 1 -element & the carrier of R in FinSETS implies R in M )
assume that
A32: the carrier of R is 1 -element and
A33: the carrier of R in FinSETS ; :: thesis: R in M
A34: R is trivial RelStr by A32;
R is Element of fin_RelStr_sp by A32, A33, Def5;
then R in f . 0 by A3, A34;
hence R in M by A31; :: thesis: verum

end;

then A35: fin_RelStr_sp c= M by A19, Def5;
then A36: Union f = fin_RelStr_sp by A5, XBOOLE_0:def 10;
assume A37: X is not 1 -element strict RelStr ; :: thesis: 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) ) )
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

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) ) ) );
A38: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A39: S₁[n] ; :: thesis: S₁[n + 1]
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 A40: X in f . (n + 1) ; :: thesis: 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) ) )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A41: 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 A4;

per cases ( X in f . n or 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) ) ) } ) by A40, A41, XBOOLE_0:def 3;

suppose X in f . n ; :: thesis: 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) ) )

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 A39; :: thesis: verum

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: 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) ) )

then ex a being Element of fin_RelStr_sp st
( a = X & 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) ) ) ) ;
then consider R1, R2 being strict RelStr such that
A42: the carrier of R1 misses the carrier of R2 and
A43: R1 in f . n and
A44: R2 in f . n and
A45: ( X = union_of (R1,R2) or X = sum_of (R1,R2) ) ;
A46: R2 in fin_RelStr_sp by A2, A36, A44, CARD_5:2;
R1 in fin_RelStr_sp by A2, A36, A43, CARD_5:2;
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, A45, A46; :: thesis: verum

end;

end;

end;

A47: S₁[ 0 ]

proof

assume X in f . 0 ; :: thesis: 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) ) )
then consider a being Element of fin_RelStr_sp such that
A48: ( X = a & a is trivial RelStr ) by A3;
a is non empty strict RelStr by Th4;
then a is non empty trivial strict RelStr by A48;
then reconsider a = a as non empty trivial strict RelStr ;
a is 1 -element strict RelStr ;
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 A37, A48; :: thesis: verum

end;

A49: for n being Nat holds S₁[n] from NAT_1:sch 2(A47, A38);
ex y being object st
( y in dom f & X in f . y ) by A1, A35, CARD_5:2;
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 A2, A49; :: thesis: verum

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: verum