:: deftheorem Def14 defines FinOrd-Approx BAGORDER:def 14 :
for R being non empty connected Poset
for b₂ being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) holds
( b₂ = FinOrd-Approx R iff ( dom b₂ = NAT & b₂ . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds b₂ . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b₂ . n ) } ) ) );