let X be set ; :: thesis: for Y being non empty set
for E1, E2 being Subset of [:X,Y:]
for p being set st E1 c= E2 holds
X-section (E1,p) c= X-section (E2,p)
let Y be non empty set ; :: thesis: for E1, E2 being Subset of [:X,Y:]
for p being set st E1 c= E2 holds
X-section (E1,p) c= X-section (E2,p)
let E1, E2 be Subset of [:X,Y:]; :: thesis: for p being set st E1 c= E2 holds
X-section (E1,p) c= X-section (E2,p)
let p be set ; :: thesis: ( E1 c= E2 implies X-section (E1,p) c= X-section (E2,p) )
assume A1: E1 c= E2 ; :: thesis: X-section (E1,p) c= X-section (E2,p)

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

let y be set ; :: thesis: ( y in X-section (E1,p) implies y in X-section (E2,p) )
assume y in X-section (E1,p) ; :: thesis: y in X-section (E2,p)
then ex y1 being Element of Y st
( y = y1 & [p,y1] in E1 ) ;
hence y in X-section (E2,p) by A1; :: thesis: verum

end;

hence X-section (E1,p) c= X-section (E2,p) ; :: thesis: verum