let U be non empty set ; :: thesis: for A being non empty IntervalSet of U

for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds

A ^ = Inter ((Y `),(X `))

let A be non empty IntervalSet of U; :: thesis: for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds

A ^ = Inter ((Y `),(X `))

let X, Y be Subset of U; :: thesis: ( A = Inter (X,Y) & X c= Y implies A ^ = Inter ((Y `),(X `)) )

assume A1: ( A = Inter (X,Y) & X c= Y ) ; :: thesis: A ^ = Inter ((Y `),(X `))

then Inter (X,Y) = Inter ((A ``1),(A ``2)) by Th15;

then ( X = A ``1 & Y = A ``2 ) by Th6, A1;

hence A ^ = Inter ((Y `),(X `)) by Th41; :: thesis: verum

for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds

A ^ = Inter ((Y `),(X `))

let A be non empty IntervalSet of U; :: thesis: for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds

A ^ = Inter ((Y `),(X `))

let X, Y be Subset of U; :: thesis: ( A = Inter (X,Y) & X c= Y implies A ^ = Inter ((Y `),(X `)) )

assume A1: ( A = Inter (X,Y) & X c= Y ) ; :: thesis: A ^ = Inter ((Y `),(X `))

then Inter (X,Y) = Inter ((A ``1),(A ``2)) by Th15;

then ( X = A ``1 & Y = A ``2 ) by Th6, A1;

hence A ^ = Inter ((Y `),(X `)) by Th41; :: thesis: verum