defpred S1[ set , set ] means ex y being Element of L st
( \$1 = y & \$2 = () /\ B );
set P = InclPoset (Ids ());
A1: for x being Element of L ex z being Element of (InclPoset (Ids ())) st S1[x,z]
proof
let x be Element of L; :: thesis: ex z being Element of (InclPoset (Ids ())) st S1[x,z]
reconsider y = x as Element of L ;
A2: the carrier of () = B by YELLOW_0:def 15;
Bottom L in B by Def8;
then (waybelow y) /\ B is Ideal of () by ;
then reconsider z = () /\ B as Element of (InclPoset (Ids ())) by YELLOW_2:41;
take z ; :: thesis: S1[x,z]
take y ; :: thesis: ( x = y & z = () /\ B )
thus ( x = y & z = () /\ B ) ; :: thesis: verum
end;
ex f being Function of the carrier of L, the carrier of (InclPoset (Ids ())) st
for x being Element of L holds S1[x,f . x] from then consider f being Function of the carrier of L, the carrier of (InclPoset (Ids ())) such that
A3: for x being Element of L ex y being Element of L st
( x = y & f . x = () /\ B ) ;
reconsider f = f as Function of L,(InclPoset (Ids ())) ;
take f ; :: thesis: for x being Element of L holds f . x = () /\ B
now :: thesis: for x being Element of L holds f . x = () /\ B
let x be Element of L; :: thesis: f . x = () /\ B
ex y being Element of L st
( x = y & f . x = () /\ B ) by A3;
hence f . x = () /\ B ; :: thesis: verum
end;
hence for x being Element of L holds f . x = () /\ B ; :: thesis: verum