A1: rng (X --> (Bottom L)) c= the carrier of L ;
( the carrier of (L |^ X) = Funcs X,the carrier of L & dom (X --> (Bottom L)) = X ) by FUNCT_2:def 1, YELLOW_1:28;
then reconsider f = X --> (Bottom L) as Element of (L |^ X) by A1, FUNCT_2:def 2;
take f ; :: according to YELLOW_0:def 4 :: thesis: f is_<=_than the carrier of (L |^ X)
let g be Element of (L |^ X); :: according to LATTICE3:def 8 :: thesis: ( not g in the carrier of (L |^ X) or f <= g )

per cases ( X is empty or not X is empty ) ;

suppose A2: X is empty ; :: thesis: ( not g in the carrier of (L |^ X) or f <= g )

A3: f <= f ;
( L |^ X = RelStr(# {{} },(id {{} }) #) & f = {} ) by A2, YELLOW_1:27;
hence ( not g in the carrier of (L |^ X) or f <= g ) by A3, TARSKI:def 1; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ( not g in the carrier of (L |^ X) or f <= g )

then reconsider X = X as non empty set ;
reconsider f = f, g = g as Element of (L |^ X) ;

now

let x be Element of X; :: thesis: f . x <= g . x
f . x = Bottom L by FUNCOP_1:13;
hence f . x <= g . x by YELLOW_0:44; :: thesis: verum

end;

hence ( not g in the carrier of (L |^ X) or f <= g ) by WAYBEL27:14; :: thesis: verum

end;

end;