let F1, F2 be finite Subset of (Bags n); :: thesis:
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:
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:

now :: thesis:

let u be object ; :: thesis:
assume A28: u in F1 ; :: thesis:
then reconsider u9 = u as Element of Bags n ;

now :: thesis:

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

now :: thesis:

let x be object ; :: thesis:
assume A30: x in F2 ; :: thesis:
then reconsider x9 = x as Element of Bags n ;

now :: thesis:

per cases ;

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

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

end;

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

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:

end;

end;

end;

hence x in F1 ; :: thesis:

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:

end;

hence u in F2 ; :: thesis:

end;

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