set L = RelStr(# (Bags n),T #);

now

let x, y be Element of RelStr(# (Bags n),T #); :: thesis: ( x <= y or y <= x )
A1: T is_connected_in field T by RELAT_2:def 14;
reconsider x' = x as bag of by POLYNOM1:def 14;
x' <= x',T by TERMORD:6;
then [x',x'] in T by TERMORD:def 2;
then A2: x in field T by RELAT_1:30;
reconsider y' = y as bag of by POLYNOM1:def 14;
y' <= y',T by TERMORD:6;
then [y',y'] in T by TERMORD:def 2;
then A3: y in field T by RELAT_1:30;

now

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 A1, A2, A3, RELAT_2:def 6;
hence ( x <= y or y <= x ) by ORDERS_2:def 9; :: thesis: verum

end;

case x = y ; :: thesis: ( x <= y or y <= x )

then x' <= y',T by TERMORD:6;
then [x',y'] in the InternalRel of RelStr(# (Bags n),T #) by TERMORD:def 2;
hence ( x <= y or y <= x ) by ORDERS_2:def 9; :: 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