:: deftheorem defines form_upper_lower_partition_of ORDERS_4:def 3 :
for L being RelStr
for A, B being set holds
( A,B form_upper_lower_partition_of L iff ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) ) );