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