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 Def4;
consider C being Subset of U such that
a2: A = Inter C,(A ``2 ) by Def5;
A ``1 = C by Pik, a2, a1;
hence A ``1 c= A ``2 by NEmptyInter, a2; :: thesis: verum