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