set L = RelStr(# (Bags n),T #);
now :: thesis: for x, y being Element of RelStr(# (Bags n),T #) holds
( x <= y or y <= x )
let x, y be Element of RelStr(# (Bags n),T #); :: thesis: ( x <= y or y <= x )
reconsider x9 = x as bag of n ;
reconsider y9 = y as bag of n ;
y9 <= y9,T by TERMORD:6;
then [y9,y9] in T by TERMORD:def 2;
then A1: y in field T by RELAT_1:15;
x9 <= x9,T by TERMORD:6;
then [x9,x9] in T by TERMORD:def 2;
then A2: ( T is_connected_in field T & x in field T ) by RELAT_1:15, RELAT_2:def 14;
now :: thesis: ( ( x <> y & ( x <= y or y <= x ) ) or ( x = y & ( x <= y or y <= x ) ) )
per cases ( x <> y or x = y ) ;
case x <> y ; :: thesis: ( x <= y or y <= x )
then ( [x,y] in the InternalRel of RelStr(# (Bags n),T #) or [y,x] in the InternalRel of RelStr(# (Bags n),T #) ) by A2, A1, RELAT_2:def 6;
hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum
end;
case x = y ; :: thesis: ( x <= y or y <= x )
then x9 <= y9,T by TERMORD:6;
then [x9,y9] in the InternalRel of RelStr(# (Bags n),T #) by TERMORD:def 2;
hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum
end;
end;
end;
hence ( x <= y or y <= x ) ; :: thesis: verum
end;
hence RelStr(# (Bags n),T #) is connected by WAYBEL_0:def 29; :: thesis: verum