A1: rng (X --> ()) c= the carrier of L ;
( the carrier of (L |^ X) = Funcs (X, the carrier of L) & dom (X --> ()) = X ) by YELLOW_1:28;
then reconsider f = X --> () as Element of (L |^ X) by ;
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(# ,() #) & f = {} ) by ;
hence ( not g in the carrier of (L |^ X) or f <= g ) by ; :: 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 :: thesis: for x being Element of X holds f . x <= g . x
let x be Element of X; :: thesis: f . x <= g . x
thus 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;