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 :: thesis: for u being object st u in F1 holds
u in F2

let u be object ; :: 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 :: thesis: u9 in F2

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

now :: thesis: for x being object st x in F2 holds
x in F1

let x be object ; :: 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 :: thesis: ( ( u9 <= x9,T & x9 in F1 ) or ( not u9 <= x9,T & x9 in F1 ) )

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 ;
then F2 c< F1 by A28, A29, XBOOLE_0:def 8;
hence contradiction by A23, A26, CARD_2:48; :: thesis: verum

end;

hence u in F2 ; :: thesis: verum

end;

then F1 c= F2 ;
hence F1 = F2 by A23, A26, CARD_2:102; :: thesis: verum