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;

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

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

then reconsider X = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) by TARSKI:def 3;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;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

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

[x,x] in X

[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_{1}[ 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_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[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;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

[x,x] in union (rng (FinOrd-Approx R));

A6: S

proof

A7:
for n being Nat st S
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;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

S

proof

A11:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[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_{1}[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))

end;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

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 <> {} )
;

end;

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;hence [y,y] in union (rng (FinOrd-Approx R)) by A5, TARSKI:def 4; :: thesis: verum

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;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

reconsider xx = x as set by TARSKI:1;

card x9 = card xx ;

hence [x,x] in X by A11; :: thesis: verum

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

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_{1}[ 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;

_{1}[ 0 ]
;

_{1}[n] holds

S_{1}[n + 1]
;

A30: for n being Nat holds S_{1}[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;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

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

then A19:
Sa = 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;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

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

then A29:
for n being Nat st Sa = 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_{4} = b_{5} )

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_{4} = b_{5}

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_{2} = b_{3} )

assume that

A21: card a = n + 1 and

A22: [a,b] in X and

A23: [b,a] in X ; :: thesis: b_{2} = b_{3}

end;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

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

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

assume that

A21: card a = n + 1 and

A22: [a,b] in X and

A23: [b,a] in X ; :: thesis: 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;

end;

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

end;

now :: thesis: a = bend;

hence
a = b
; :: thesis: verumper 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;

end;

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

end;

now :: thesis: a = bend;

hence
a = b
; :: thesis: verumper 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;

end;

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

end;

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;

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

hence a = b by A26, A27, A28, XBOOLE_1:45; :: thesis: verum

end;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

then
{(PosetMax a)} c= a
;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;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

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

then
{(PosetMax b)} c= b
;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;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

hence a = b by A26, A27, A28, XBOOLE_1:45; :: thesis: verum

S

A30: for n being Nat holds S

reconsider xx = x as set by TARSKI:1;

card x9 = card xx ;

hence x = y by A14, A15, A16, A30; :: thesis: verum

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

A53:
X is_reflexive_in Fin the carrier of R
by A3;[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_{1}[ 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;

_{1}[ 0 ]
;

_{1}[n] holds

S_{1}[n + 1]
;

A52: for n being Nat holds S_{1}[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;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

[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

then A38:
S[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;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

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

then A51:
for n being Nat st S[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_{5},b_{7}] 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_{5},b_{7}] 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_{2},b_{4}] in X )

assume that

A40: card a = n + 1 and

A41: [a,b] in X and

A42: [b,c] in X ; :: thesis: [b_{2},b_{4}] in X

end;[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

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

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

assume that

A40: card a = n + 1 and

A41: [a,b] in X and

A42: [b,c] in X ; :: thesis: [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 union (rng (FinOrd-Approx R)) ) )
by A41, Th32;

end;

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

end;

now :: thesis: [a,c] in Xend;

hence
[a,c] in X
; :: thesis: verumper 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;

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;

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

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

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

end;

now :: thesis: [a,c] in Xend;

hence
[a,c] in X
; :: thesis: verumper 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;

end;

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

end;

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;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

S

A52: for n being Nat holds S

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

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