let F1, F2 be finite Subset of (Bags n); :: thesis: ( F1 c= Support p & card F1 = i & ( for b, b9 being bag of n st b in F1 & b9 in Support p & b <= b9,T holds
b9 in F1 ) & F2 c= Support p & card F2 = i & ( for b, b9 being bag of n st b in F2 & b9 in Support p & b <= b9,T holds
b9 in F2 ) implies F1 = F2 )
assume that
A22: F1 c= Support p and
A23: card F1 = i and
A24: for b, b9 being bag of n st b in F1 & b9 in Support p & b <= b9,T holds
b9 in F1 ; :: thesis: ( not F2 c= Support p or not card F2 = i or ex b, b9 being bag of n st
( b in F2 & b9 in Support p & b <= b9,T & not b9 in F2 ) or F1 = F2 )
assume that
A25: F2 c= Support p and
A26: card F2 = i and
A27: for b, b9 being bag of n st b in F2 & b9 in Support p & b <= b9,T holds
b9 in F2 ; :: thesis: F1 = F2

now

let u be set ; :: thesis: ( u in F1 implies u in F2 )
assume A28: u in F1 ; :: thesis: u in F2
then reconsider u9 = u as Element of Bags n ;

now

assume A29: not u9 in F2 ; :: thesis: contradiction

now

let x be set ; :: thesis: ( x in F2 implies x in F1 )
assume A30: x in F2 ; :: thesis: x in F1
then reconsider x9 = x as Element of Bags n ;

now

per cases ( u9 <= x9,T or not u9 <= x9,T ) ;

case u9 <= x9,T ; :: thesis: x9 in F1

hence x9 in F1 by A24, A25, A28, A30; :: thesis: verum

end;

case not u9 <= x9,T ; :: thesis: x9 in F1

then x9 < u9,T by TERMORD:5;
then x9 <= u9,T by TERMORD:def 3;
hence x9 in F1 by A22, A27, A28, A29, A30; :: thesis: verum

end;

end;

end;

hence x in F1 ; :: thesis: verum

end;

then F2 c= F1 by TARSKI:def 3;
then F2 c< F1 by A28, A29, XBOOLE_0:def 8;
hence contradiction by A23, A26, CARD_2:67; :: thesis: verum

end;

hence u in F2 ; :: thesis: verum

end;

then F1 c= F2 by TARSKI:def 3;
hence F1 = F2 by A23, A26, PRE_POLY:8; :: thesis: verum