let R be non empty connected Poset; for x, y being Element of Fin the carrier of R holds
( [x,y] in union (rng (FinOrd-Approx R)) iff ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) ) )
let x, y be Element of Fin the carrier of R; ( [x,y] in union (rng (FinOrd-Approx R)) iff ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) ) )
set IR = the InternalRel of R;
set CR = the carrier of R;
set FOAR = FinOrd-Approx 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;
A2:
dom (FinOrd-Approx R) = NAT
by Def14;
hereby ( ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) ) implies [x,y] in union (rng (FinOrd-Approx R)) )
assume
[x,y] in union (rng (FinOrd-Approx R))
;
( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )then consider Y being
set such that A3:
[x,y] in Y
and A4:
Y in rng (FinOrd-Approx R)
by TARSKI:def 4;
consider n being
object such that A5:
n in dom (FinOrd-Approx R)
and A6:
Y = (FinOrd-Approx R) . n
by A4, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A5;
per cases
( n = 0 or n > 0 )
;
suppose
n = 0
;
( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )then consider a,
b being
Element of
Fin the
carrier of
R such that A7:
[x,y] = [a,b]
and A8:
(
a = {} or (
a <> {} &
b <> {} &
PosetMax a <> PosetMax b &
[(PosetMax a),(PosetMax b)] in the
InternalRel of
R ) )
by A1, A3, A6;
x = a
by A7, XTUPLE_0:1;
hence
(
x = {} or (
x <> {} &
y <> {} &
PosetMax x <> PosetMax y &
[(PosetMax x),(PosetMax y)] in the
InternalRel of
R ) or (
x <> {} &
y <> {} &
PosetMax x = PosetMax y &
[(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )
by A7, A8, XTUPLE_0:1;
verum end; suppose
n > 0
;
( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )then A9:
n - 1 is
Element of
NAT
by NAT_1:20;
then
(FinOrd-Approx R) . ((n - 1) + 1) = { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in (FinOrd-Approx R) . (n - 1) ) }
by Def14;
then consider a,
b being
Element of
Fin the
carrier of
R such that A10:
[x,y] = [a,b]
and
a <> {}
and A11:
b <> {}
and A12:
PosetMax a = PosetMax b
and A13:
[(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in (FinOrd-Approx R) . (n - 1)
by A3, A6;
A14:
x = a
by A10, XTUPLE_0:1;
A15:
y = b
by A10, XTUPLE_0:1;
(FinOrd-Approx R) . (n - 1) in rng (FinOrd-Approx R)
by A2, A9, FUNCT_1:def 3;
hence
(
x = {} or (
x <> {} &
y <> {} &
PosetMax x <> PosetMax y &
[(PosetMax x),(PosetMax y)] in the
InternalRel of
R ) or (
x <> {} &
y <> {} &
PosetMax x = PosetMax y &
[(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )
by A11, A12, A13, A14, A15, TARSKI:def 4;
verum end;
end;
assume A16:
( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )
; [x,y] in union (rng (FinOrd-Approx R))
per cases
( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) )
by A16;
suppose A19:
(
x <> {} &
y <> {} &
PosetMax x = PosetMax y &
[(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) )
;
[x,y] in union (rng (FinOrd-Approx R))set NEXTXY =
[(x \ {(PosetMax x)}),(y \ {(PosetMax y)})];
consider Y being
set such that A20:
[(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in Y
and A21:
Y in rng (FinOrd-Approx R)
by A19, TARSKI:def 4;
consider n being
object such that A22:
n in dom (FinOrd-Approx R)
and A23:
Y = (FinOrd-Approx R) . n
by A21, FUNCT_1:def 3;
reconsider n =
n as
Nat by A22;
(FinOrd-Approx R) . (n + 1) = { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in (FinOrd-Approx R) . n ) }
by Def14;
then A24:
[x,y] in (FinOrd-Approx R) . (n + 1)
by A19, A20, A23;
(FinOrd-Approx R) . (n + 1) in rng (FinOrd-Approx R)
by A2, FUNCT_1:def 3;
hence
[x,y] in union (rng (FinOrd-Approx R))
by A24, TARSKI:def 4;
verum end;