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

(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