defpred S₁[ set ] means ( $1 in X & B1 in $1 );
set LB = { B2 where B2 is Element of A : S₁[B2] } ;
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S₁[B2] } by A1, A2, Th8;
then A3: inf { B2 where B2 is Element of A : S₁[B2] } in { B2 where B2 is Element of A : S₁[B2] } by ORDINAL2:17;
S₁[ inf { B2 where B2 is Element of A : S₁[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