let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being bag of the carrier of R
for x, y being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 & a . y > 0 & x <> y holds
x ## y
let a, b be bag of the carrier of R; :: thesis: for x, y being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 & a . y > 0 & x <> y holds
x ## y
let x, y be Element of R; :: thesis: for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 & a . y > 0 & x <> y holds
x ## y
let p be partition of b -' a; :: thesis: for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 & a . y > 0 & x <> y holds
x ## y
let q be partition of b; :: thesis: ( q is ordered & q = <*a*> ^ p & a . x > 0 & a . y > 0 & x <> y implies x ## y )
assume Z0: q is ordered ; :: thesis: ( not q = <*a*> ^ p or not a . x > 0 or not a . y > 0 or not x <> y or x ## y )
assume Z1: q = <*a*> ^ p ; :: thesis: ( not a . x > 0 or not a . y > 0 or not x <> y or x ## y )
assume Z2: ( a . x > 0 & a . y > 0 ) ; :: thesis: ( not x <> y or x ## y )
( 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 ( not x <> y or x ## y ) by Z0, Z2; :: thesis: verum