set T = { x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } ;
{ x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } c= the carrier of W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } or x in the carrier of W )
assume x in { x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } ; :: thesis: x in the carrier of W
then consider x1 being Element of W such that
A1: ( x1 = x & ( ( a <= x1 & x1 <= b ) or ( b <= x1 & x1 <= a ) ) ) ;
thus x in the carrier of W by A1; :: thesis: verum

end;

hence { x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } is Subset of W ; :: thesis: verum