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 a0: ( A = Inter X,Y & X c= Y ) ; :: thesis: A ^ = Inter (Y ` ),(X ` )
Inter X,Y = Inter (A ``1 ),(A ``2 ) by Wazne33, a0;
then ( X = A ``1 & Y = A ``2 ) by Pik, a0;
hence A ^ = Inter (Y ` ),(X ` ) by Dif2; :: thesis: verum