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;

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 17;

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

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;

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 17;

A3: now :: thesis: for b9 being bag of n st b9 in P holds

b <= b9,T

MinElement (P,RelStr(# (Bags n),T #)) in P
by BAGORDER:def 17;b <= b9,T

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:15;

b9 <= b9,T by TERMORD:6;

then [b9,b9] in T by TERMORD:def 2;

then A5: b9 in field T by RELAT_1:15;

assume A6: b9 in P ; :: thesis: b <= b9,T

end;b <= b,T by TERMORD:6;

then [b,b] in T by TERMORD:def 2;

then A4: b in field T by RELAT_1:15;

b9 <= b9,T by TERMORD:6;

then [b9,b9] in T by TERMORD:def 2;

then A5: b9 in field T by RELAT_1:15;

assume A6: b9 in P ; :: thesis: b <= b9,T

now :: thesis: ( ( b9 = b & b <= b9,T ) or ( b9 <> b & b <= b9,T ) )

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

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