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;
A3: now :: thesis: for b9 being bag of n st b9 in P holds
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
now :: thesis: ( ( b9 = b & b <= b9,T ) or ( b9 <> b & b <= b9,T ) )
per cases ( b9 = b or b9 <> b ) ;
case b9 = b ; :: thesis: b <= b9,T
hence b <= b9,T by TERMORD:6; :: thesis: verum
end;
end;
end;
hence b <= b9,T ; :: thesis: verum
end;
MinElement (P,RelStr(# (Bags n),T #)) in P 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