reconsider f = X --> (Bottom L) as Element of (ContMaps (X,L)) by WAYBEL24:21;
take
f
; YELLOW_0:def 4 f is_<=_than the carrier of (ContMaps (X,L))
let g be Element of (ContMaps (X,L)); LATTICE3:def 8 ( not g in the carrier of (ContMaps (X,L)) or f <= g )
A1:
ContMaps (X,L) is full SubRelStr of L |^ the carrier of X
by WAYBEL24:def 3;
then reconsider a = g as Element of (L |^ the carrier of X) by YELLOW_0:58;
A2:
TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) = TopStruct(# the carrier of X, the topology of X #)
by WAYBEL25:def 2;
then (Omega X) --> (Bottom L) =
the carrier of X --> (Bottom L)
.=
X --> (Bottom L)
;
then
( a >= Bottom (L |^ the carrier of X) & Bottom (L |^ the carrier of X) = f )
by A2, WAYBEL24:33, YELLOW_0:44;
hence
( not g in the carrier of (ContMaps (X,L)) or f <= g )
by A1, YELLOW_0:60; verum