let R be non empty connected Poset; 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 Def16;
then reconsider X = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) by TARSKI:def 3;
A13:
now let x,
y be
set ;
( 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 A14:
x in Fin the
carrier of
R
and A15:
y in Fin the
carrier of
R
and A16:
[x,y] in X
and A17:
[y,x] in X
;
x = yreconsider x9 =
x as
Element of
Fin the
carrier of
R by A14;
defpred S1[
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;
then A20:
S1[
0 ]
;
now let n be
Nat;
( ( 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
b4 = b5 )assume A21:
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
;
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
b4 = b5let a,
b be
Element of
Fin the
carrier of
R;
( card a = n + 1 & [a,b] in X & [b,a] in X implies b2 = b3 )assume that A22:
card a = n + 1
and A23:
[a,b] in X
and A24:
[b,a] in X
;
b2 = b3 end; then A30:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
;
A31:
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A20, A30);
consider n being
Nat such that A32:
x,
n are_equipotent
by A14, CARD_1:74;
card x9 = n
by A32, CARD_1:def 5;
hence
x = y
by A15, A16, A17, A31;
verum end;
A33:
now let x,
y,
z be
set ;
( 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 A34:
x in Fin the
carrier of
R
and A35:
y in Fin the
carrier of
R
and A36:
z in Fin the
carrier of
R
and A37:
[x,y] in X
and A38:
[y,z] in X
;
[x,z] in Xdefpred S1[
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;
then A40:
S1[
0 ]
;
now let n be
Nat;
( ( 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
[b5,b7] in X )assume A41:
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
;
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
[b5,b7] in Xlet a,
b,
c be
Element of
Fin the
carrier of
R;
( card a = n + 1 & [a,b] in X & [b,c] in X implies [b2,b4] in X )assume that A42:
card a = n + 1
and A43:
[a,b] in X
and A44:
[b,c] in X
;
[b2,b4] in Xper 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 A43, Th36;
suppose A48:
(
a <> {} &
b <> {} &
PosetMax a = PosetMax b &
[(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in union (rng (FinOrd-Approx R)) )
;
[b2,b4] in Xnow 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 A44, Th36;
suppose A49:
(
b <> {} &
c <> {} &
PosetMax b = PosetMax c &
[(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) )
;
[a,c] in Xset z =
a \ {(PosetMax a)};
reconsider z =
a \ {(PosetMax a)} as
Element of
Fin the
carrier of
R by Th38;
A50:
card z = n
by A42, Lm1;
A51:
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 A51, XBOOLE_1:1;
then reconsider zc =
c9 \ {(PosetMax c)} as
Element of
Fin the
carrier of
R by FINSUB_1:def 5;
A52:
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 A52, XBOOLE_1:1;
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 A48;
then
[z,zc] in union (rng (FinOrd-Approx R))
by A41, A49, A50;
hence
[a,c] in X
by A48, A49, Th36;
verum end; hence
[a,c] in X
;
verum end; then A53:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
;
A54:
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A40, A53);
reconsider x9 =
x as
Element of
Fin the
carrier of
R by A34;
consider n being
Nat such that A55:
x,
n are_equipotent
by A34, CARD_1:74;
card x9 = n
by A55, CARD_1:def 5;
hence
[x,z] in X
by A35, A36, A37, A38, A54;
verum end;
A56:
X is_reflexive_in Fin the carrier of R
by A3, RELAT_2:def 1;
A57:
X is_antisymmetric_in Fin the carrier of R
by A13, RELAT_2:def 4;
A58:
X is_transitive_in Fin the carrier of R
by A33, RELAT_2:def 8;
reconsider R = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) by A3;
A59:
dom R = Fin the carrier of R
by A56, ORDERS_1:98;
field R = Fin the carrier of R
by A56, ORDERS_1:98;
hence
union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)
by A56, A57, A58, A59, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; verum