set R = RelStr(# (Bags n),T #);
set X = the carrier of RelStr(# (Bags n),T #);
now :: thesis: for Y being set st Y c= the carrier of RelStr(# (Bags n),T #) & Y <> {} holds
ex a being object st
( a in Y & T -Seg a misses Y )
let Y be set ; :: thesis: ( Y c= the carrier of RelStr(# (Bags n),T #) & Y <> {} implies ex a being object st
( a in Y & T -Seg a misses Y ) )
assume that
A1: Y c= the carrier of RelStr(# (Bags n),T #) and
A2: Y <> {} ; :: thesis: ex a being object st
( a in Y & T -Seg a misses Y )
now :: thesis: for u being object st u in Y holds
u in field T
let u be object ; :: thesis: ( u in Y implies u in field T )
assume u in Y ; :: thesis: u in field T
then reconsider u9 = u as bag of n by A1;
u9 <= u9,T by TERMORD:6;
then [u9,u9] in T by TERMORD:def 2;
hence u in field T by RELAT_1:15; :: thesis: verum
end;
then Y c= field T by TARSKI:def 3;
hence ex a being object st
( a in Y & T -Seg a misses Y ) by A2, WELLORD1:def 2; :: thesis: verum
end;
then T is_well_founded_in the carrier of RelStr(# (Bags n),T #) by WELLORD1:def 3;
hence RelStr(# (Bags n),T #) is well_founded by WELLFND1:def 2; :: thesis: verum