defpred S_{1}[ set ] means ( $1 in X & B1 in $1 );

set LB = { B2 where B2 is Element of A : S_{1}[B2] } ;

ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S_{1}[B2] }
by A1, A2, Th8;

then A3: inf { B2 where B2 is Element of A : S_{1}[B2] } in { B2 where B2 is Element of A : S_{1}[B2] }
by ORDINAL2:17;

S_{1}[ inf { B2 where B2 is Element of A : S_{1}[B2] } ]
from CARD_FIL:sch 1(A3);

hence inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X ; :: thesis: verum

set LB = { B2 where B2 is Element of A : S

ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S

then A3: inf { B2 where B2 is Element of A : S

S

hence inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X ; :: thesis: verum