set IT = UNION (A,B);
consider A1, A2 being Subset of U such that
A3: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
consider B1, B2 being Subset of U such that
A4: ( B1 c= B2 & B = Inter (B1,B2) ) by Th11;
set LAB = A1 \/ B1;
set UAB = A2 \/ B2;
UNION (A,B) = Inter ((A1 \/ B1),(A2 \/ B2)) by Th13, A3, A4;
hence UNION (A,B) is IntervalSet of U ; :: thesis: verum