let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A ``1 c= A ``2
let A be non empty IntervalSet of U; :: thesis: A ``1 c= A ``2
consider B being Subset of U such that
A1: A = Inter ((A ``1),B) by Def5;
consider C being Subset of U such that
A2: A = Inter (C,(A ``2)) by Def6;
A ``1 = C by Th6, A2, A1;
hence A ``1 c= A ``2 by Th5, A2; :: thesis: verum