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

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