let X, Y be TopSpace; :: thesis: for A being Subset of X st [#] X c= [#] Y holds
(incl (X,Y)) .: A = A
let A be Subset of X; :: thesis: ( [#] X c= [#] Y implies (incl (X,Y)) .: A = A )
assume [#] X c= [#] Y ; :: thesis: (incl (X,Y)) .: A = A
hence (incl (X,Y)) .: A = (id ([#] X)) .: A by YELLOW_9:def 1
.= A by FUNCT_1:92 ;
:: thesis: verum