theorem Th36: :: BAGORDER:39

for R being non empty connected Poset
for a, b being Element of (FinPoset R) holds
( [a,b] in the InternalRel of (FinPoset R) iff ex x, y being Element of Fin the carrier of R st
( a = x & b = y & ( 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 FinOrd R ) ) ) )