let F1, F2 be finite Subset of ; :: thesis: ( F1 c= Support p & card F1 = i & ( for b, b' being bag of n st b in F1 & b' in Support p & b <= b',T holds
b' in F1 ) & F2 c= Support p & card F2 = i & ( for b, b' being bag of n st b in F2 & b' in Support p & b <= b',T holds
b' in F2 ) implies F1 = F2 )
assume that
A22: F1 c= Support p and
A23: card F1 = i and
A24: for b, b' being bag of n st b in F1 & b' in Support p & b <= b',T holds
b' in F1 ; :: thesis: ( not F2 c= Support p or not card F2 = i or ex b, b' being bag of n st
( b in F2 & b' in Support p & b <= b',T & not b' in F2 ) or F1 = F2 )
assume that
A25: F2 c= Support p and
A26: card F2 = i and
A27: for b, b' being bag of n st b in F2 & b' in Support p & b <= b',T holds
b' 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 u' = u as Element of Bags n ;

now

assume A29: not u' 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 x' = x as Element of Bags n ;

now

per cases ( u' <= x',T or not u' <= x',T ) ;

case u' <= x',T ; :: thesis: x' in F1

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

end;

case not u' <= x',T ; :: thesis: x' in F1

then x' < u',T by TERMORD:5;
then x' <= u',T by TERMORD:def 3;
hence x' 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