let R be non empty connected Poset; :: thesis: for x being Element of Fin the carrier of R st x <> {} holds
not [x,{}] in union (rng (FinOrd-Approx R))
let x be Element of Fin the carrier of R; :: thesis: ( x <> {} implies not [x,{}] in union (rng (FinOrd-Approx R)) )
assume A1: x <> {} ; :: thesis: not [x,{}] in union (rng (FinOrd-Approx R))
set CR = the carrier of R;
set FOAR = FinOrd-Approx R;
reconsider y = {} as Element of Fin the carrier of R by FINSUB_1:7;

now :: thesis: not [x,y] in union (rng (FinOrd-Approx R))

assume A2: [x,y] in union (rng (FinOrd-Approx R)) ; :: thesis: contradiction

per cases ( x = {} or ( x <> {} & y <> {} & [(PosetMax x),(PosetMax y)] in the carrier of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ (PosetMax x)),({} \ (PosetMax y))] in union (rng (FinOrd-Approx R)) ) ) by A2, Th32;

suppose x = {} ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ( x <> {} & y <> {} & [(PosetMax x),(PosetMax y)] in the carrier of R ) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

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

hence contradiction ; :: thesis: verum

end;

end;

end;

hence not [x,{}] in union (rng (FinOrd-Approx R)) ; :: thesis: verum