let R be non empty connected Poset; :: thesis: union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)
set IR = the InternalRel of R;
set CR = the carrier of R;
set X = union (rng (FinOrd-Approx R));
set FOAR = FinOrd-Approx R;
set FOAR0 = { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ;
A1: (FinOrd-Approx R) . 0 = { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } by Def14;

now :: thesis: for x being object st x in union (rng (FinOrd-Approx R)) holds
x in [:(Fin the carrier of R),(Fin the carrier of R):]

let x be object ; :: thesis: ( x in union (rng (FinOrd-Approx R)) implies x in [:(Fin the carrier of R),(Fin the carrier of R):] )
assume x in union (rng (FinOrd-Approx R)) ; :: thesis: x in [:(Fin the carrier of R),(Fin the carrier of R):]
then A2: ex Y being set st
( x in Y & Y in rng (FinOrd-Approx R) ) by TARSKI:def 4;
rng (FinOrd-Approx R) c= bool [:(Fin the carrier of R),(Fin the carrier of R):] by RELAT_1:def 19;
hence x in [:(Fin the carrier of R),(Fin the carrier of R):] by A2; :: thesis: verum

end;

then reconsider X = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) by TARSKI:def 3;

A3: now :: thesis: for x being object st x in Fin the carrier of R holds
[x,x] in X

let x be object ; :: thesis: ( x in Fin the carrier of R implies [x,x] in X )
assume A4: x in Fin the carrier of R ; :: thesis: [x,x] in X
0 in NAT ;
then 0 in dom (FinOrd-Approx R) by Def14;
then A5: (FinOrd-Approx R) . 0 in rng (FinOrd-Approx R) by FUNCT_1:def 3;
reconsider x9 = x as Element of Fin the carrier of R by A4;
defpred S₁[ Nat] means for x being Element of Fin the carrier of R st card x = $1 holds
[x,x] in union (rng (FinOrd-Approx R));
A6: S₁[ 0 ]

proof

let x be Element of Fin the carrier of R; :: thesis: ( card x = 0 implies [x,x] in union (rng (FinOrd-Approx R)) )
assume card x = 0 ; :: thesis: [x,x] in union (rng (FinOrd-Approx R))
then x = {} ;
then [x,x] in (FinOrd-Approx R) . 0 by A1;
hence [x,x] in union (rng (FinOrd-Approx R)) by A5, TARSKI:def 4; :: thesis: verum

end;

A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: for x being Element of Fin the carrier of R st card x = n holds
[x,x] in union (rng (FinOrd-Approx R)) ; :: thesis: S₁[n + 1]
let y be Element of Fin the carrier of R; :: thesis: ( card y = n + 1 implies [y,y] in union (rng (FinOrd-Approx R)) )
assume A9: card y = n + 1 ; :: thesis: [y,y] in union (rng (FinOrd-Approx R))

per cases ( y = {} or y <> {} ) ;

suppose y = {} ; :: thesis: [y,y] in union (rng (FinOrd-Approx R))

then [y,y] in (FinOrd-Approx R) . 0 by A1;
hence [y,y] in union (rng (FinOrd-Approx R)) by A5, TARSKI:def 4; :: thesis: verum

end;

suppose A10: y <> {} ; :: thesis: [y,y] in union (rng (FinOrd-Approx R))

set z = y \ {(PosetMax y)};
reconsider z = y \ {(PosetMax y)} as Element of Fin the carrier of R by Th34;
card z = n by A9, Lm1;
then [z,z] in union (rng (FinOrd-Approx R)) by A8;
hence [y,y] in union (rng (FinOrd-Approx R)) by A10, Th32; :: thesis: verum

end;

end;

end;

A11: for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
reconsider xx = x as set by TARSKI:1;
card x9 = card xx ;
hence [x,x] in X by A11; :: thesis: verum

end;

A12: now :: thesis: for x, y being object st x in Fin the carrier of R & y in Fin the carrier of R & [x,y] in X & [y,x] in X holds
x = y

let x, y be object ; :: thesis: ( x in Fin the carrier of R & y in Fin the carrier of R & [x,y] in X & [y,x] in X implies x = y )
assume that
A13: x in Fin the carrier of R and
A14: y in Fin the carrier of R and
A15: [x,y] in X and
A16: [y,x] in X ; :: thesis: x = y
reconsider x9 = x as Element of Fin the carrier of R by A13;
defpred S₁[ Nat] means for x, y being Element of Fin the carrier of R st card x = $1 & [x,y] in X & [y,x] in X holds
x = y;

now :: thesis: for a, b being Element of Fin the carrier of R st card a = 0 & [a,b] in X & [b,a] in X holds
a = b

let a, b be Element of Fin the carrier of R; :: thesis: ( card a = 0 & [a,b] in X & [b,a] in X implies a = b )
assume that
A17: card a = 0 and
[a,b] in X and
A18: [b,a] in X ; :: thesis: a = b
reconsider a9 = a as finite set ;
a9 = {} by A17;
hence a = b by A18, Th33; :: thesis: verum

end;

then A19: S₁[ 0 ] ;

now :: thesis: for n being Nat st ( for a, b being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,a] in X holds
a = b ) holds
for a, b being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,a] in X holds
a = b

let n be Nat; :: thesis: ( ( for a, b being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,a] in X holds
a = b ) implies for a, b being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,a] in X holds
b₄ = b₅ )
assume A20: for a, b being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,a] in X holds
a = b ; :: thesis: for a, b being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,a] in X holds
b₄ = b₅
let a, b be Element of Fin the carrier of R; :: thesis: ( card a = n + 1 & [a,b] in X & [b,a] in X implies b₂ = b₃ )
assume that
A21: card a = n + 1 and
A22: [a,b] in X and
A23: [b,a] in X ; :: thesis: b₂ = b₃

per cases ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) or ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in X ) ) by A22, Th32;

suppose a = {} ; :: thesis: b₂ = b₃

hence a = b by A21; :: thesis: verum

end;

suppose A24: ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ; :: thesis: b₂ = b₃

now :: thesis: a = b

per cases ( b = {} or ( b <> {} & a <> {} & PosetMax b <> PosetMax a & [(PosetMax b),(PosetMax a)] in the InternalRel of R ) or ( b <> {} & a <> {} & PosetMax b = PosetMax a & [(b \ {(PosetMax b)}),(a \ {(PosetMax a)})] in X ) ) by A23, Th32;

suppose b = {} ; :: thesis: a = b

hence a = b by A24; :: thesis: verum

end;

suppose ( b <> {} & a <> {} & PosetMax b <> PosetMax a & [(PosetMax b),(PosetMax a)] in the InternalRel of R ) ; :: thesis: a = b

hence a = b by A24, ORDERS_1:4; :: thesis: verum

end;

suppose ( b <> {} & a <> {} & PosetMax b = PosetMax a & [(b \ {(PosetMax b)}),(a \ {(PosetMax a)})] in X ) ; :: thesis: a = b

hence a = b by A24; :: thesis: verum

end;

end;

end;

hence a = b ; :: thesis: verum

end;

suppose A25: ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in X ) ; :: thesis: b₂ = b₃

now :: thesis: a = b

per cases ( b = {} or ( b <> {} & a <> {} & PosetMax b <> PosetMax a & [(PosetMax b),(PosetMax a)] in the InternalRel of R ) or ( b <> {} & a <> {} & PosetMax b = PosetMax a & [(b \ {(PosetMax b)}),(a \ {(PosetMax a)})] in X ) ) by A23, Th32;

suppose b = {} ; :: thesis: a = b

hence a = b by A25; :: thesis: verum

end;

suppose ( b <> {} & a <> {} & PosetMax b <> PosetMax a & [(PosetMax b),(PosetMax a)] in the InternalRel of R ) ; :: thesis: a = b

hence a = b by A25; :: thesis: verum

end;

suppose A26: ( b <> {} & a <> {} & PosetMax b = PosetMax a & [(b \ {(PosetMax b)}),(a \ {(PosetMax a)})] in X ) ; :: thesis: a = b

reconsider a9 = a as finite set ;
reconsider b9 = b as finite set ;
set za = a9 \ {(PosetMax a)};
set zb = b9 \ {(PosetMax b)};
reconsider za = a9 \ {(PosetMax a)}, zb = b9 \ {(PosetMax b)} as Element of Fin the carrier of R by Th34;
card za = n by A21, Lm1;
then A27: za = zb by A20, A25, A26;

now :: thesis: for z being object st z in {(PosetMax a)} holds
z in a

let z be object ; :: thesis: ( z in {(PosetMax a)} implies z in a )
assume z in {(PosetMax a)} ; :: thesis: z in a
then z = PosetMax a by TARSKI:def 1;
hence z in a by A26, Def13; :: thesis: verum

end;

then {(PosetMax a)} c= a ;
then A28: a = {(PosetMax a)} \/ za by XBOOLE_1:45;

now :: thesis: for z being object st z in {(PosetMax b)} holds
z in b

let z be object ; :: thesis: ( z in {(PosetMax b)} implies z in b )
assume z in {(PosetMax b)} ; :: thesis: z in b
then z = PosetMax b by TARSKI:def 1;
hence z in b by A26, Def13; :: thesis: verum

end;

then {(PosetMax b)} c= b ;
hence a = b by A26, A27, A28, XBOOLE_1:45; :: thesis: verum

end;

end;

end;

hence a = b ; :: thesis: verum

end;

end;

end;

then A29: for n being Nat st S₁[n] holds
S₁[n + 1] ;
A30: for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A29);
reconsider xx = x as set by TARSKI:1;
card x9 = card xx ;
hence x = y by A14, A15, A16, A30; :: thesis: verum

end;

A31: now :: thesis: for x, y, z being object st x in Fin the carrier of R & y in Fin the carrier of R & z in Fin the carrier of R & [x,y] in X & [y,z] in X holds
[x,z] in X

let x, y, z be object ; :: thesis: ( x in Fin the carrier of R & y in Fin the carrier of R & z in Fin the carrier of R & [x,y] in X & [y,z] in X implies [x,z] in X )
assume that
A32: x in Fin the carrier of R and
A33: y in Fin the carrier of R and
A34: z in Fin the carrier of R and
A35: [x,y] in X and
A36: [y,z] in X ; :: thesis: [x,z] in X
defpred S₁[ Nat] means for a, b, c being Element of Fin the carrier of R st card a = $1 & [a,b] in X & [b,c] in X holds
[a,c] in X;

now :: thesis: for a, b, c being Element of Fin the carrier of R st card a = 0 & [a,b] in X & [b,c] in X holds
[a,c] in X

let a, b, c be Element of Fin the carrier of R; :: thesis: ( card a = 0 & [a,b] in X & [b,c] in X implies [a,c] in X )
assume that
A37: card a = 0 and
[a,b] in X and
[b,c] in X ; :: thesis: [a,c] in X
reconsider a9 = a as finite set ;
a9 = {} by A37;
hence [a,c] in X by Th32; :: thesis: verum

end;

then A38: S₁[ 0 ] ;

now :: thesis: for n being Nat st ( for a, b, c being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,c] in X holds
[a,c] in X ) holds
for a, b, c being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,c] in X holds
[a,c] in X

let n be Nat; :: thesis: ( ( for a, b, c being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,c] in X holds
[a,c] in X ) implies for a, b, c being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,c] in X holds
[b₅,b₇] in X )
assume A39: for a, b, c being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,c] in X holds
[a,c] in X ; :: thesis: for a, b, c being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,c] in X holds
[b₅,b₇] in X
let a, b, c be Element of Fin the carrier of R; :: thesis: ( card a = n + 1 & [a,b] in X & [b,c] in X implies [b₂,b₄] in X )
assume that
A40: card a = n + 1 and
A41: [a,b] in X and
A42: [b,c] in X ; :: thesis: [b₂,b₄] in X

per cases ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) or ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in union (rng (FinOrd-Approx R)) ) ) by A41, Th32;

suppose a = {} ; :: thesis: [b₂,b₄] in X

hence [a,c] in X by Th32; :: thesis: verum

end;

suppose A43: ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ; :: thesis: [b₂,b₄] in X

now :: thesis: [a,c] in X

per cases ( b = {} or ( b <> {} & c <> {} & PosetMax b <> PosetMax c & [(PosetMax b),(PosetMax c)] in the InternalRel of R ) or ( b <> {} & c <> {} & PosetMax b = PosetMax c & [(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) ) ) by A42, Th32;

suppose b = {} ; :: thesis: [a,c] in X

hence [a,c] in X by A43; :: thesis: verum

end;

suppose A44: ( b <> {} & c <> {} & PosetMax b <> PosetMax c & [(PosetMax b),(PosetMax c)] in the InternalRel of R ) ; :: thesis: [a,c] in X

then A45: [(PosetMax a),(PosetMax c)] in the InternalRel of R by A43, ORDERS_1:5;

now :: thesis: [a,c] in X

per cases ( PosetMax a <> PosetMax c or PosetMax a = PosetMax c ) ;

suppose PosetMax a <> PosetMax c ; :: thesis: [a,c] in X

hence [a,c] in X by A43, A44, A45, Th32; :: thesis: verum

end;

suppose PosetMax a = PosetMax c ; :: thesis: [a,c] in X

hence [a,c] in X by A43, A44, ORDERS_1:4; :: thesis: verum

end;

end;

end;

hence [a,c] in X ; :: thesis: verum

end;

suppose ( b <> {} & c <> {} & PosetMax b = PosetMax c & [(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) ) ; :: thesis: [a,c] in X

hence [a,c] in X by A43, Th32; :: thesis: verum

end;

end;

end;

hence [a,c] in X ; :: thesis: verum

end;

suppose A46: ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in union (rng (FinOrd-Approx R)) ) ; :: thesis: [b₂,b₄] in X

now :: thesis: [a,c] in X

per cases ( b = {} or ( b <> {} & c <> {} & PosetMax b <> PosetMax c & [(PosetMax b),(PosetMax c)] in the InternalRel of R ) or ( b <> {} & c <> {} & PosetMax b = PosetMax c & [(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) ) ) by A42, Th32;

suppose b = {} ; :: thesis: [a,c] in X

hence [a,c] in X by A46; :: thesis: verum

end;

suppose ( b <> {} & c <> {} & PosetMax b <> PosetMax c & [(PosetMax b),(PosetMax c)] in the InternalRel of R ) ; :: thesis: [a,c] in X

hence [a,c] in X by A46, Th32; :: thesis: verum

end;

suppose A47: ( b <> {} & c <> {} & PosetMax b = PosetMax c & [(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) ) ; :: thesis: [a,c] in X

set z = a \ {(PosetMax a)};
reconsider z = a \ {(PosetMax a)} as Element of Fin the carrier of R by Th34;
A48: card z = n by A40, Lm1;
A49: c c= the carrier of R by FINSUB_1:def 5;
reconsider c9 = c as finite set ;
set zc = c9 \ {(PosetMax c)};
c9 \ {(PosetMax c)} c= the carrier of R by A49;
then reconsider zc = c9 \ {(PosetMax c)} as Element of Fin the carrier of R by FINSUB_1:def 5;
A50: b c= the carrier of R by FINSUB_1:def 5;
reconsider b9 = b as finite set ;
set zb = b9 \ {(PosetMax b)};
b9 \ {(PosetMax b)} c= the carrier of R by A50;
then reconsider zb = b9 \ {(PosetMax b)} as Element of Fin the carrier of R by FINSUB_1:def 5;
[z,zb] in union (rng (FinOrd-Approx R)) by A46;
then [z,zc] in union (rng (FinOrd-Approx R)) by A39, A47, A48;
hence [a,c] in X by A46, A47, Th32; :: thesis: verum

end;

end;

end;

hence [a,c] in X ; :: thesis: verum

end;

end;

end;

then A51: for n being Nat st S₁[n] holds
S₁[n + 1] ;
A52: for n being Nat holds S₁[n] from NAT_1:sch 2(A38, A51);
reconsider x9 = x as Element of Fin the carrier of R by A32;
reconsider xx = x as set by TARSKI:1;
card x9 = card xx ;
hence [x,z] in X by A33, A34, A35, A36, A52; :: thesis: verum

end;

A53: X is_reflexive_in Fin the carrier of R by A3;
A54: X is_antisymmetric_in Fin the carrier of R by A12;
A55: X is_transitive_in Fin the carrier of R by A31;
reconsider R = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) by A3;
A56: dom R = Fin the carrier of R by A53, ORDERS_1:13;
field R = Fin the carrier of R by A53, ORDERS_1:13;
hence union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R) by A53, A54, A55, A56, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum