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
A1: A _/\_ A c= A

proof

let x be object ; :: 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
A2: ( X in A & Y in A & x = X /\ Y ) by SETFAM_1:def 5;
A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;
( A ``1 c= Y & Y c= A ``2 ) by A2, Th14;
then A4: A ``1 c= X /\ Y by A3, XBOOLE_1:19;
X /\ Y c= X by XBOOLE_1:17;
then X /\ Y c= A ``2 by A3;
hence x in A by A4, A2, Th14; :: thesis: verum

end;

A c= A _/\_ A

proof

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

end;

hence A _/\_ A = A by A1; :: thesis: verum