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

now

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

now

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

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

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

end;

case A5: b' <> b ; :: thesis: b <= b',T

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

end;

end;

end;

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

end;

hence ex b being bag of st
( b in P & ( for b' being bag of st b' in P holds
b <= b',T ) ) by A1; :: thesis: verum