let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A = Inter ((A ``1),(A ``2))
let A be non empty IntervalSet of U; :: thesis: A = Inter ((A ``1),(A ``2))
A1: Inter ((A ``1),(A ``2)) c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter ((A ``1),(A ``2)) or x in A )
reconsider xx = x as set by TARSKI:1;
assume x in Inter ((A ``1),(A ``2)) ; :: thesis: x in A
then ( A ``1 c= xx & xx c= A ``2 ) by Th1;
hence x in A by Th14; :: thesis: verum
end;
A c= Inter ((A ``1),(A ``2))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Inter ((A ``1),(A ``2)) )
reconsider xx = x as set by TARSKI:1;
assume x in A ; :: thesis: x in Inter ((A ``1),(A ``2))
then ( A ``1 c= xx & xx c= A ``2 ) by Th14;
hence x in Inter ((A ``1),(A ``2)) by Th1; :: thesis: verum
end;
hence A = Inter ((A ``1),(A ``2)) by A1; :: thesis: verum