reconsider f = X --> (Bottom L) as Element of (ContMaps (X,L)) by WAYBEL24:21;
take f ; :: according to YELLOW_0:def 4 :: thesis: f is_<=_than the carrier of (ContMaps (X,L))
let g be Element of (ContMaps (X,L)); :: according to LATTICE3:def 8 :: thesis: ( 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; :: thesis: verum