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

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