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 or [p,y1] in E2 ) by A2, XBOOLE_0:def 3;
then ( q in X-section (E1,p) or q in X-section (E2,p) ) by A2;
hence q in (X-section (E1,p)) \/ (X-section (E2,p)) by XBOOLE_0:def 3; :: 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 b₁ in X-section ((E1 \/ E2),p) )
assume A4: q in (X-section (E1,p)) \/ (X-section (E2,p)) ; :: thesis: b₁ in X-section ((E1 \/ E2),p)

per cases ( q in X-section (E1,p) or q in X-section (E2,p) ) by A4, XBOOLE_0:def 3;

suppose q in X-section (E1,p) ; :: thesis: b₁ in X-section ((E1 \/ E2),p)

then consider y1 being Element of Y such that
A5: ( q = y1 & [p,y1] in E1 ) ;
[p,y1] in E1 \/ E2 by A5, XBOOLE_0:def 3;
hence q in X-section ((E1 \/ E2),p) by A5; :: thesis: verum

end;

suppose q in X-section (E2,p) ; :: thesis: b₁ in X-section ((E1 \/ E2),p)

then consider y1 being Element of Y such that
A6: ( q = y1 & [p,y1] in E2 ) ;
[p,y1] in E1 \/ E2 by A6, XBOOLE_0:def 3;
hence q in X-section ((E1 \/ E2),p) by A6; :: thesis: verum

end;

end;

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 or [x1,p] in E2 ) by A2, XBOOLE_0:def 3;
then ( q in Y-section (E1,p) or q in Y-section (E2,p) ) by A2;
hence q in (Y-section (E1,p)) \/ (Y-section (E2,p)) by XBOOLE_0:def 3; :: 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 b₁ in Y-section ((E1 \/ E2),p) )
assume A4: q in (Y-section (E1,p)) \/ (Y-section (E2,p)) ; :: thesis: b₁ in Y-section ((E1 \/ E2),p)

per cases ( q in Y-section (E1,p) or q in Y-section (E2,p) ) by A4, XBOOLE_0:def 3;

suppose q in Y-section (E1,p) ; :: thesis: b₁ in Y-section ((E1 \/ E2),p)

then consider x1 being Element of X such that
A5: ( q = x1 & [x1,p] in E1 ) ;
[x1,p] in E1 \/ E2 by A5, XBOOLE_0:def 3;
hence q in Y-section ((E1 \/ E2),p) by A5; :: thesis: verum

end;

suppose q in Y-section (E2,p) ; :: thesis: b₁ in Y-section ((E1 \/ E2),p)

then consider x1 being Element of X such that
A6: ( q = x1 & [x1,p] in E2 ) ;
[x1,p] in E1 \/ E2 by A6, XBOOLE_0:def 3;
hence q in Y-section ((E1 \/ E2),p) by A6; :: thesis: verum

end;

end;

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