let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for P being non empty Subset of (Bags n) ex b being bag of n st
( b in P & ( for b9 being bag of n st b9 in P holds
b <= b9,T ) )
let T be connected admissible TermOrder of n; :: thesis: for P being non empty Subset of (Bags n) ex b being bag of n st
( b in P & ( for b9 being bag of n st b9 in P holds
b <= b9,T ) )
let P be non empty Subset of (Bags n); :: thesis: ex b being bag of n st
( b in P & ( for b9 being bag of n st b9 in P holds
b <= b9,T ) )
set R = RelStr(# (Bags n),T #);
set m = MinElement P,RelStr(# (Bags n),T #);
A1: T is_connected_in field T by RELAT_2:def 14;
MinElement P,RelStr(# (Bags n),T #) is Element of Bags n ;
then reconsider b = MinElement P,RelStr(# (Bags n),T #) as bag of n ;
A2: MinElement P,RelStr(# (Bags n),T #) is_minimal_wrt P,the InternalRel of RelStr(# (Bags n),T #) by BAGORDER:def 19;

A3: now

let b9 be bag of n; :: thesis: ( b9 in P implies b <= b9,T )
b <= b,T by TERMORD:6;
then [b,b] in T by TERMORD:def 2;
then A4: b in field T by RELAT_1:30;
b9 <= b9,T by TERMORD:6;
then [b9,b9] in T by TERMORD:def 2;
then A5: b9 in field T by RELAT_1:30;
assume A6: b9 in P ; :: thesis: b <= b9,T

now

per cases ( b9 = b or b9 <> b ) ;

case b9 = b ; :: thesis: b <= b9,T

hence b <= b9,T by TERMORD:6; :: thesis: verum

end;

case A7: b9 <> b ; :: thesis: b <= b9,T

then not [b9,b] in T by A2, A6, WAYBEL_4:def 26;
then [b,b9] in T by A1, A4, A5, A7, RELAT_2:def 6;
hence b <= b9,T by TERMORD:def 2; :: thesis: verum

end;

end;

end;

hence b <= b9,T ; :: thesis: verum

end;

MinElement P,RelStr(# (Bags n),T #) in P by BAGORDER:def 19;
hence ex b being bag of n st
( b in P & ( for b9 being bag of n st b9 in P holds
b <= b9,T ) ) by A3; :: thesis: verum