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) ) )

A1 in Inter (A1,A2) by A3;

hence A is non empty IntervalSet of U by A3; :: thesis: verum

( 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 )

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 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;( 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

A1 in Inter (A1,A2) by A3;

hence A is non empty IntervalSet of U by A3; :: thesis: verum