defpred S_{1}[ set , set ] means ex y being Element of L st

( $1 = y & $2 = (waybelow y) /\ B );

set P = InclPoset (Ids (subrelstr B));

A1: for x being Element of L ex z being Element of (InclPoset (Ids (subrelstr B))) st S_{1}[x,z]

for x being Element of L holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

then consider f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) such that

A3: for x being Element of L ex y being Element of L st

( x = y & f . x = (waybelow y) /\ B ) ;

reconsider f = f as Function of L,(InclPoset (Ids (subrelstr B))) ;

take f ; :: thesis: for x being Element of L holds f . x = (waybelow x) /\ B

( $1 = y & $2 = (waybelow y) /\ B );

set P = InclPoset (Ids (subrelstr B));

A1: for x being Element of L ex z being Element of (InclPoset (Ids (subrelstr B))) st S

proof

ex f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) st
let x be Element of L; :: thesis: ex z being Element of (InclPoset (Ids (subrelstr B))) st S_{1}[x,z]

reconsider y = x as Element of L ;

A2: the carrier of (subrelstr B) = B by YELLOW_0:def 15;

Bottom L in B by Def8;

then (waybelow y) /\ B is Ideal of (subrelstr B) by A2, Th50;

then reconsider z = (waybelow y) /\ B as Element of (InclPoset (Ids (subrelstr B))) by YELLOW_2:41;

take z ; :: thesis: S_{1}[x,z]

take y ; :: thesis: ( x = y & z = (waybelow y) /\ B )

thus ( x = y & z = (waybelow y) /\ B ) ; :: thesis: verum

end;reconsider y = x as Element of L ;

A2: the carrier of (subrelstr B) = B by YELLOW_0:def 15;

Bottom L in B by Def8;

then (waybelow y) /\ B is Ideal of (subrelstr B) by A2, Th50;

then reconsider z = (waybelow y) /\ B as Element of (InclPoset (Ids (subrelstr B))) by YELLOW_2:41;

take z ; :: thesis: S

take y ; :: thesis: ( x = y & z = (waybelow y) /\ B )

thus ( x = y & z = (waybelow y) /\ B ) ; :: thesis: verum

for x being Element of L holds S

then consider f being Function of the carrier of L, the carrier of (InclPoset (Ids (subrelstr B))) such that

A3: for x being Element of L ex y being Element of L st

( x = y & f . x = (waybelow y) /\ B ) ;

reconsider f = f as Function of L,(InclPoset (Ids (subrelstr B))) ;

take f ; :: thesis: for x being Element of L holds f . x = (waybelow x) /\ B

now :: thesis: for x being Element of L holds f . x = (waybelow x) /\ B

hence
for x being Element of L holds f . x = (waybelow x) /\ B
; :: thesis: verumlet x be Element of L; :: thesis: f . x = (waybelow x) /\ B

ex y being Element of L st

( x = y & f . x = (waybelow y) /\ B ) by A3;

hence f . x = (waybelow x) /\ B ; :: thesis: verum

end;ex y being Element of L st

( x = y & f . x = (waybelow y) /\ B ) by A3;

hence f . x = (waybelow x) /\ B ; :: thesis: verum