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))
b1: Inter ((A ``1),(A ``2)) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter ((A ``1),(A ``2)) or x in A )
assume x in Inter ((A ``1),(A ``2)) ; :: thesis: x in A
then ( A ``1 c= x & x c= A ``2 ) by Lemacik;
hence x in A by Wazne; :: thesis: verum

end;

A c= Inter ((A ``1),(A ``2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Inter ((A ``1),(A ``2)) )
assume x in A ; :: thesis: x in Inter ((A ``1),(A ``2))
then ( A ``1 c= x & x c= A ``2 ) by Wazne;
hence x in Inter ((A ``1),(A ``2)) by Lemacik; :: thesis: verum

end;

hence A = Inter ((A ``1),(A ``2)) by b1, XBOOLE_0:def 10; :: thesis: verum