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 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) ;
for x being Element of X holds f . x <= g . x by YELLOW_0:44;
hence ( not g in the carrier of (L |^ X) or f <= g ) by WAYBEL27:14; :: thesis: verum

end;

end;