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

now

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

now

assume A20: not u' in F2 ; :: thesis: contradiction

now

let x be set ; :: thesis: ( x in F2 implies x in F1 )
assume A21: 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 A17, A18, A19, A21; :: 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 A17, A18, A19, A20, A21; :: 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 A19, A20, XBOOLE_0:def 8;
hence contradiction by A17, A18, 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 A17, A18, TRIANG_1:3; :: thesis: verum