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₁ 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₁ . W = (W, the carrier of X) *graph ; :: thesis: verum