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