consider F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,(Sigma (InclPoset the topology of Y))) such that
F is monotone and
A1: for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph by WAYBEL26:46;
Omega (Sigma (InclPoset the topology of Y)) = Sigma (InclPoset the topology of Y) by WAYBEL25:15;
then oContMaps X,(Sigma (InclPoset the topology of Y)) = ContMaps X,(Sigma (InclPoset the topology of Y)) by 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 by A1; :: thesis: verum