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 ; :: thesis: verum

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 ; :: thesis: verum