let X be non empty set ; :: thesis: for Y being set
for E1, E2 being Subset of [:X,Y:]
for p being set st E1 c= E2 holds
Y-section (E1,p) c= Y-section (E2,p)
let Y be set ; :: thesis: for E1, E2 being Subset of [:X,Y:]
for p being set st E1 c= E2 holds
Y-section (E1,p) c= Y-section (E2,p)
let E1, E2 be Subset of [:X,Y:]; :: thesis: for p being set st E1 c= E2 holds
Y-section (E1,p) c= Y-section (E2,p)
let p be set ; :: thesis: ( E1 c= E2 implies Y-section (E1,p) c= Y-section (E2,p) )
assume A1: E1 c= E2 ; :: thesis: Y-section (E1,p) c= Y-section (E2,p)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y-section (E1,p) or y in Y-section (E2,p) )
assume y in Y-section (E1,p) ; :: thesis: y in Y-section (E2,p)
then ex y1 being Element of X st
( y = y1 & [y1,p] in E1 ) ;
hence y in Y-section (E2,p) by A1; :: thesis: verum