let X, Y be non empty set ; :: thesis: for E1, E2 being Subset of [:X,Y:]
for p being set holds
( X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) & Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) )
let E1, E2 be Subset of [:X,Y:]; :: thesis: for p being set holds
( X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) & Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) )
let p be set ; :: thesis: ( X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) & Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) )

now :: thesis: for q being set st q in X-section ((E1 /\ E2),p) holds
q in (X-section (E1,p)) /\ (X-section (E2,p))

let q be set ; :: thesis: ( q in X-section ((E1 /\ E2),p) implies q in (X-section (E1,p)) /\ (X-section (E2,p)) )
assume q in X-section ((E1 /\ E2),p) ; :: thesis: q in (X-section (E1,p)) /\ (X-section (E2,p))
then consider y1 being Element of Y such that
A2: ( q = y1 & [p,y1] in E1 /\ E2 ) ;
( [p,y1] in E1 & [p,y1] in E2 ) by A2, XBOOLE_0:def 4;
then ( q in X-section (E1,p) & q in X-section (E2,p) ) by A2;
hence q in (X-section (E1,p)) /\ (X-section (E2,p)) by XBOOLE_0:def 4; :: thesis: verum

end;

then A3: X-section ((E1 /\ E2),p) c= (X-section (E1,p)) /\ (X-section (E2,p)) ;

now :: thesis: for q being set st q in (X-section (E1,p)) /\ (X-section (E2,p)) holds
q in X-section ((E1 /\ E2),p)

let q be set ; :: thesis: ( q in (X-section (E1,p)) /\ (X-section (E2,p)) implies q in X-section ((E1 /\ E2),p) )
assume q in (X-section (E1,p)) /\ (X-section (E2,p)) ; :: thesis: q in X-section ((E1 /\ E2),p)
then A4: ( q in X-section (E1,p) & q in X-section (E2,p) ) by XBOOLE_0:def 4;
then consider y1 being Element of Y such that
A5: ( q = y1 & [p,y1] in E1 ) ;
consider y2 being Element of Y such that
A6: ( q = y2 & [p,y2] in E2 ) by A4;
[p,q] in E1 /\ E2 by A5, A6, XBOOLE_0:def 4;
hence q in X-section ((E1 /\ E2),p) by A5; :: thesis: verum

end;

then (X-section (E1,p)) /\ (X-section (E2,p)) c= X-section ((E1 /\ E2),p) ;
hence X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) by A3; :: thesis: Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p))

now :: thesis: for q being set st q in Y-section ((E1 /\ E2),p) holds
q in (Y-section (E1,p)) /\ (Y-section (E2,p))

let q be set ; :: thesis: ( q in Y-section ((E1 /\ E2),p) implies q in (Y-section (E1,p)) /\ (Y-section (E2,p)) )
assume q in Y-section ((E1 /\ E2),p) ; :: thesis: q in (Y-section (E1,p)) /\ (Y-section (E2,p))
then consider x1 being Element of X such that
A2: ( q = x1 & [x1,p] in E1 /\ E2 ) ;
( [x1,p] in E1 & [x1,p] in E2 ) by A2, XBOOLE_0:def 4;
then ( q in Y-section (E1,p) & q in Y-section (E2,p) ) by A2;
hence q in (Y-section (E1,p)) /\ (Y-section (E2,p)) by XBOOLE_0:def 4; :: thesis: verum

end;

then A3: Y-section ((E1 /\ E2),p) c= (Y-section (E1,p)) /\ (Y-section (E2,p)) ;

now :: thesis: for q being set st q in (Y-section (E1,p)) /\ (Y-section (E2,p)) holds
q in Y-section ((E1 /\ E2),p)

let q be set ; :: thesis: ( q in (Y-section (E1,p)) /\ (Y-section (E2,p)) implies q in Y-section ((E1 /\ E2),p) )
assume q in (Y-section (E1,p)) /\ (Y-section (E2,p)) ; :: thesis: q in Y-section ((E1 /\ E2),p)
then A4: ( q in Y-section (E1,p) & q in Y-section (E2,p) ) by XBOOLE_0:def 4;
then consider x1 being Element of X such that
A5: ( q = x1 & [x1,p] in E1 ) ;
consider x2 being Element of X such that
A6: ( q = x2 & [x2,p] in E2 ) by A4;
[x1,p] in E1 /\ E2 by A5, A6, XBOOLE_0:def 4;
hence q in Y-section ((E1 /\ E2),p) by A5; :: thesis: verum

end;

then (Y-section (E1,p)) /\ (Y-section (E2,p)) c= Y-section ((E1 /\ E2),p) ;
hence Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) by A3; :: thesis: verum