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