Omega (Sigma (InclPoset the topology of Y)) = Sigma (InclPoset the topology of Y)
by WAYBEL25:15;

then ( ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,(Sigma (InclPoset the topology of Y)))) st

( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) ) & oContMaps (X,(Sigma (InclPoset the topology of Y))) = ContMaps (X,(Sigma (InclPoset the topology of Y))) ) by WAYBEL26:45, WAYBEL26:def 1;

hence ex b_{1} being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st

for W being open Subset of [:X,Y:] holds b_{1} . W = (W, the carrier of X) *graph
; :: thesis: verum

then ( ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,(Sigma (InclPoset the topology of Y)))) st

( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) ) & oContMaps (X,(Sigma (InclPoset the topology of Y))) = ContMaps (X,(Sigma (InclPoset the topology of Y))) ) by WAYBEL26:45, WAYBEL26:def 1;

hence ex b

for W being open Subset of [:X,Y:] holds b