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:162 ;
:: thesis: verum