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 A1: 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
A2: A = Inter (A1,A2) by Def2;
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 A1, A2, Th3; :: thesis: A = Inter (A1,A2)
thus A = Inter (A1,A2) by A2; :: thesis: verum

end;

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