let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for P being non empty Subset of ex b being bag of n st
( b in P & ( for b' being bag of n st b' in P holds
b <= b',T ) )
let T be connected admissible TermOrder of n; :: thesis: for P being non empty Subset of ex b being bag of n st
( b in P & ( for b' being bag of n st b' in P holds
b <= b',T ) )
let P be non empty Subset of ; :: thesis: ex b being bag of n st
( b in P & ( for b' being bag of n st b' in P holds
b <= b',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 b' be bag of n; :: thesis: ( b' in P implies b <= b',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;
b' <= b',T by TERMORD:6;
then [b',b'] in T by TERMORD:def 2;
then A5: b' in field T by RELAT_1:30;
assume A6: b' in P ; :: thesis: b <= b',T

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 A7: b' <> b ; :: thesis: b <= b',T

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

end;

end;

end;

hence b <= b',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 b' being bag of n st b' in P holds
b <= b',T ) ) by A3; :: thesis: verum