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:59;
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:61; :: thesis: verum