let I be set ; :: thesis: for m, n being bag of I holds
( m -' n <> EmptyBag I or m = n or n -' m <> EmptyBag I )
let m, n be bag of I; :: thesis: ( m -' n <> EmptyBag I or m = n or n -' m <> EmptyBag I )
assume Z0: m -' n = EmptyBag I ; :: thesis: ( m = n or n -' m <> EmptyBag I )
assume m <> n ; :: thesis: n -' m <> EmptyBag I
then consider a being object such that
A1: ( a in I & m . a <> n . a ) by PBOOLE:def 10;
per cases ( m . a > n . a or n . a > m . a ) by A1, XXREAL_0:1;
suppose m . a > n . a ; :: thesis: n -' m <> EmptyBag I
then (m . a) - (n . a) > 0 by XREAL_1:50;
then (m . a) -' (n . a) > 0 by XREAL_0:def 2;
then ( 0 < (m -' n) . a & (m -' n) . a = 0 ) by A1, Z0, FUNCOP_1:7, PRE_POLY:def 6;
hence n -' m <> EmptyBag I ; :: thesis: verum
end;
suppose A3: n . a > m . a ; :: thesis: n -' m <> EmptyBag I
take a ; :: according to PBOOLE:def 10 :: thesis: ( a in I & not (n -' m) . a = (EmptyBag I) . a )
thus a in I by A1; :: thesis: not (n -' m) . a = (EmptyBag I) . a
(n . a) - (m . a) > 0 by A3, XREAL_1:50;
then (n . a) -' (m . a) > 0 by XREAL_0:def 2;
then (n -' m) . a > 0 by PRE_POLY:def 6;
hence (n -' m) . a <> (EmptyBag I) . a by A1, FUNCOP_1:7; :: thesis: verum
end;
end;