let U be non empty set ; :: thesis: for A being non empty IntervalSet of U
for X being set holds
( X in A iff ( A ``1 c= X & X c= A ``2 ) )
let A be non empty IntervalSet of U; :: thesis: for X being set holds
( X in A iff ( A ``1 c= X & X c= A ``2 ) )
let X be set ; :: thesis: ( X in A iff ( A ``1 c= X & X c= A ``2 ) )
A1: ( X in A implies ( A ``1 c= X & X c= A ``2 ) )

proof

assume A2: X in A ; :: thesis: ( A ``1 c= X & X c= A ``2 )
A3: A ``1 c= X

proof

consider B being Subset of U such that
A4: A = Inter ((A ``1),B) by Def5;
thus A ``1 c= X by Th1, A2, A4; :: thesis: verum

end;

X c= A ``2

proof

consider B being Subset of U such that
A5: A = Inter (B,(A ``2)) by Def6;
thus X c= A ``2 by Th1, A2, A5; :: thesis: verum

end;

hence ( A ``1 c= X & X c= A ``2 ) by A3; :: thesis: verum

end;

( A ``1 c= X & X c= A ``2 implies X in A )

proof

assume ( A ``1 c= X & X c= A ``2 ) ; :: thesis: X in A
then A6: X in Inter ((A ``1),(A ``2)) by Th1;
consider B being Subset of U such that
A7: A = Inter ((A ``1),B) by Def5;
consider C being Subset of U such that
A8: A = Inter (C,(A ``2)) by Def6;
thus X in A by A7, A6, Th6, A8; :: thesis: verum

end;

hence ( X in A iff ( A ``1 c= X & X c= A ``2 ) ) by A1; :: thesis: verum