let b1, b2 be Element of Bags n; :: thesis: ( ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) & ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) implies b1 = b2 )
set O = T;
assume A30: ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) ; :: thesis: ( ( not ( Support p = {} & b2 = EmptyBag n ) & not ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) or b1 = b2 )
assume A31: ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) ; :: thesis: b1 = b2
per cases ( Support p = {} or Support p <> {} ) ;
suppose Support p = {} ; :: thesis: b1 = b2
hence b1 = b2 by A30, A31; :: thesis: verum
end;
suppose A32: Support p <> {} ; :: thesis: b1 = b2
then b1 <= b2,T by A30, A31;
then A33: [b1,b2] in T ;
b2 <= b1,T by A30, A31, A32;
then [b2,b1] in T ;
hence b1 = b2 by A33, ORDERS_1:4; :: thesis: verum
end;
end;