let R be non empty transitive asymmetric RelStr ; :: thesis: for b being bag of the carrier of R holds
( b = EmptyBag the carrier of R iff OrderedPartition b = {} )
let b be bag of the carrier of R; :: thesis: ( b = EmptyBag the carrier of R iff OrderedPartition b = {} )
set I = the carrier of R;
set E = EmptyBag the carrier of R;
set p = OrderedPartition b;
consider F, G being Function of NAT,(Bags the carrier of R) such that
A1: ( F . 0 = b & G . 0 = EmptyBag the carrier of R & ( for i being Nat holds
( G . (i + 1) = (F . i) | { x where x is Element of R : x is_maximal_in support (F . i) } & F . (i + 1) = (F . i) -' (G . (i + 1)) ) ) & ex i being Nat st
( F . i = EmptyBag the carrier of R & OrderedPartition b = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) by OP;
consider i being Nat such that
A2: ( F . i = EmptyBag the carrier of R & OrderedPartition b = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) by A1;
hereby :: thesis: ( OrderedPartition b = {} implies b = EmptyBag the carrier of R )
assume b = EmptyBag the carrier of R ; :: thesis: OrderedPartition b = {}
then i <= 0 by A1, A2;
then i = 0 ;
hence OrderedPartition b = {} by A2; :: thesis: verum
end;
assume OrderedPartition b = {} ; :: thesis: b = EmptyBag the carrier of R
then OrderedPartition b = <*> (Bags the carrier of R) ;
then Sum (OrderedPartition b) = EmptyBag the carrier of R by Th21;
hence b = EmptyBag the carrier of R by PART; :: thesis: verum