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:46, 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