let R be non empty connected Poset; :: thesis: 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; :: thesis: ( [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 Def16;
A2: dom (FinOrd-Approx R) = NAT by Def16;

hereby :: thesis: ( ( 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)) ; :: thesis: ( 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 & Y in rng (FinOrd-Approx R) ) by TARSKI:def 4;
consider n being set such that
A4: ( n in dom (FinOrd-Approx R) & Y = (FinOrd-Approx R) . n ) by A3, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A4;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ( 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
A5: [x,y] = [a,b] and
A6: ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) by A1, A3, A4;
( x = a & b = y ) by A5, ZFMISC_1:33;
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 A6; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ( 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 A7: 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 Def16;
then consider a, b being Element of Fin the carrier of R such that
A8: [x,y] = [a,b] and
A9: ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in (FinOrd-Approx R) . (n - 1) ) by A3, A4;
A10: ( x = a & y = b ) by A8, ZFMISC_1:33;
(FinOrd-Approx R) . (n - 1) in rng (FinOrd-Approx R) by A2, A7, FUNCT_1:def 5;
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 A9, A10, TARSKI:def 4; :: thesis: verum

end;

end;

end;

assume A11: ( 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)) ) ) ; :: thesis: [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 A11;

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

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

end;

suppose ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ; :: thesis: [x,y] in union (rng (FinOrd-Approx R))

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

end;

suppose A14: ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) ; :: thesis: [x,y] in union (rng (FinOrd-Approx R))

set NEXTXY = [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})];
consider Y being set such that
A15: ( [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in Y & Y in rng (FinOrd-Approx R) ) by A14, TARSKI:def 4;
consider n being set such that
A16: ( n in dom (FinOrd-Approx R) & Y = (FinOrd-Approx R) . n ) by A15, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A16;
(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 Def16;
then A17: [x,y] in (FinOrd-Approx R) . (n + 1) by A14, A15, A16;
(FinOrd-Approx R) . (n + 1) in rng (FinOrd-Approx R) by A2, FUNCT_1:def 5;
hence [x,y] in union (rng (FinOrd-Approx R)) by A17, TARSKI:def 4; :: thesis: verum

end;

end;