let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being bag of the carrier of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
a <> EmptyBag the carrier of R
let a, b be bag of the carrier of R; :: thesis: for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
a <> EmptyBag the carrier of R
let p be partition of b -' a; :: thesis: for q being partition of b st q is ordered & q = <*a*> ^ p holds
a <> EmptyBag the carrier of R
let q be partition of b; :: thesis: ( q is ordered & q = <*a*> ^ p implies a <> EmptyBag the carrier of R )
assume Z0: q is ordered ; :: thesis: ( not q = <*a*> ^ p or a <> EmptyBag the carrier of R )
assume Z1: q = <*a*> ^ p ; :: thesis: a <> EmptyBag the carrier of R
( a in {a} & {a} = rng <*a*> ) by TARSKI:def 1, FINSEQ_1:39;
then ( a in (rng <*a*>) \/ (rng p) & (rng <*a*>) \/ (rng p) = rng q ) by Z1, XBOOLE_0:def 3, FINSEQ_1:31;
hence a <> EmptyBag the carrier of R by Z0; :: thesis: verum