let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A _/\_ A = A
let A be non empty IntervalSet of U; :: thesis: A _/\_ A = A
set B = A _/\_ A;
C1: A _/\_ A c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A _/\_ A or x in A )
assume x in A _/\_ A ; :: thesis: x in A
then consider X, Y being set such that
C2: ( X in A & Y in A & x = X /\ Y ) by SETFAM_1:def 5;
C3: ( A ``1 c= X & X c= A ``2 ) by C2, Wazne;
( A ``1 c= Y & Y c= A ``2 ) by C2, Wazne;
then C4: A ``1 c= X /\ Y by C3, XBOOLE_1:19;
X /\ Y c= X by XBOOLE_1:17;
then X /\ Y c= A ``2 by C3, XBOOLE_1:1;
hence x in A by C4, C2, Wazne; :: thesis: verum

end;

A c= A _/\_ A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A _/\_ A )
assume X2: x in A ; :: thesis: x in A _/\_ A
x = x /\ x ;
hence x in A _/\_ A by X2, SETFAM_1:def 5; :: thesis: verum

end;

hence A _/\_ A = A by C1, XBOOLE_0:def 10; :: thesis: verum