let U be non empty set ; :: thesis: for A, B being non empty IntervalSet of U holds A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
let A, B be non empty IntervalSet of U; :: thesis: A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
v1: A _/\_ B c= Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))

proof

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

end;

Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) c= A _/\_ B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) or x in A _/\_ B )
assume x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) ; :: thesis: x in A _/\_ B
then consider Z being Element of bool U such that
z2: ( x = Z & (A ``1) /\ (B ``1) c= Z & Z c= (A ``2) /\ (B ``2) ) ;
A ``1 c= (Z \/ (A ``1)) /\ (A ``2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ``1 or x in (Z \/ (A ``1)) /\ (A ``2) )
assume a0: x in A ``1 ; :: thesis: x in (Z \/ (A ``1)) /\ (A ``2)
assume aa: not x in (Z \/ (A ``1)) /\ (A ``2) ; :: thesis: contradiction

per cases ( not x in Z \/ (A ``1) or not x in A ``2 ) by aa, XBOOLE_0:def 4;

suppose not x in Z \/ (A ``1) ; :: thesis: contradiction

hence contradiction by a0, XBOOLE_0:def 3; :: thesis: verum

end;

suppose b1: not x in A ``2 ; :: thesis: contradiction

( A ``1 c= A ``2 & x in A ``1 ) by a0, wazne2;
hence contradiction by b1; :: thesis: verum

end;

end;

end;

then ( A ``1 c= (Z \/ (A ``1)) /\ (A ``2) & (Z \/ (A ``1)) /\ (A ``2) c= A ``2 ) by XBOOLE_1:17;
then e1: (Z \/ (A ``1)) /\ (A ``2) in A by Wazne;
B ``1 c= (Z \/ (B ``1)) /\ (B ``2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B ``1 or x in (Z \/ (B ``1)) /\ (B ``2) )
assume a1: x in B ``1 ; :: thesis: x in (Z \/ (B ``1)) /\ (B ``2)
then a2: x in Z \/ (B ``1) by XBOOLE_0:def 3;
B ``1 c= B ``2 by wazne2;
hence x in (Z \/ (B ``1)) /\ (B ``2) by a1, a2, XBOOLE_0:def 4; :: thesis: verum

end;

then ( B ``1 c= (Z \/ (B ``1)) /\ (B ``2) & (Z \/ (B ``1)) /\ (B ``2) c= B ``2 ) by XBOOLE_1:17;
then e2: (Z \/ (B ``1)) /\ (B ``2) in B by Wazne;
((Z \/ (A ``1)) /\ (A ``2)) /\ ((Z \/ (B ``1)) /\ (B ``2)) = (((A ``2) /\ (Z \/ (A ``1))) /\ (Z \/ (B ``1))) /\ (B ``2) by XBOOLE_1:16
.= ((A ``2) /\ ((Z \/ (A ``1)) /\ (Z \/ (B ``1)))) /\ (B ``2) by XBOOLE_1:16
.= ((A ``2) /\ (Z \/ ((A ``1) /\ (B ``1)))) /\ (B ``2) by XBOOLE_1:24
.= ((A ``2) /\ Z) /\ (B ``2) by z2, XBOOLE_1:12
.= Z /\ ((A ``2) /\ (B ``2)) by XBOOLE_1:16
.= Z by z2, XBOOLE_1:28 ;
hence x in A _/\_ B by SETFAM_1:def 5, z2, e1, e2; :: thesis: verum

end;

hence A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) by v1, XBOOLE_0:def 10; :: thesis: verum