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

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

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

A3: A ``1 c= X

end;A3: A ``1 c= X

proof

X c= A ``2
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;A4: A = Inter ((A ``1),B) by Def5;

thus A ``1 c= X by Th1, A2, A4; :: thesis: verum

proof

hence
( A ``1 c= X & X c= A ``2 )
by A3; :: thesis: verum
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;A5: A = Inter (B,(A ``2)) by Def6;

thus X c= A ``2 by Th1, A2, A5; :: thesis: verum

proof

hence
( X in A iff ( A ``1 c= X & X c= A ``2 ) )
by A1; :: thesis: verum
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;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