let U be non empty set ; :: thesis: for A being set holds
( A is non empty IntervalSet of U iff ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter A1,A2 ) )
let A be set ; :: thesis: ( A is non empty IntervalSet of U iff ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter A1,A2 ) )

hereby :: thesis: ( ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter A1,A2 ) implies A is non empty IntervalSet of U )

assume A0: A is non empty IntervalSet of U ; :: thesis: ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter A1,A2 )
then consider A1, A2 being Subset of U such that
a1: A = Inter A1,A2 by WW;
take A1 = A1; :: thesis: ex A2 being Subset of U st
( A1 c= A2 & A = Inter A1,A2 )
take A2 = A2; :: thesis: ( A1 c= A2 & A = Inter A1,A2 )
thus A1 c= A2 by A0, a1, ThA2; :: thesis: A = Inter A1,A2
thus A = Inter A1,A2 by a1; :: thesis: verum

end;

given A1, A2 being Subset of U such that B1: ( A1 c= A2 & A = Inter A1,A2 ) ; :: thesis: A is non empty IntervalSet of U
A1 in Inter A1,A2 by B1;
hence A is non empty IntervalSet of U by B1; :: thesis: verum