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