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 v0: X in A ; :: thesis: ( A ``1 c= X & X c= A ``2 )
v1: A ``1 c= X

proof

consider B being Subset of U such that
v3: A = Inter ((A ``1),B) by Def4;
thus A ``1 c= X by Lemacik, v0, v3; :: thesis: verum

end;

X c= A ``2

proof

consider B being Subset of U such that
v4: A = Inter (B,(A ``2)) by Def5;
thus X c= A ``2 by Lemacik, v0, v4; :: thesis: verum

end;

hence ( A ``1 c= X & X c= A ``2 ) by v1; :: 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 v0: X in Inter ((A ``1),(A ``2)) by Lemacik;
consider B being Subset of U such that
v1: A = Inter ((A ``1),B) by Def4;
consider C being Subset of U such that
v2: A = Inter (C,(A ``2)) by Def5;
thus X in A by v1, v0, Pik, v2; :: thesis: verum

end;

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