:: deftheorem Def1 defines chain-complete POSET_1:def 1 :
for IT being RelStr holds
( IT is chain-complete iff ( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds
ex_sup_of L,IT ) ) );