let A be limit_ordinal infinite Ordinal; :: thesis: for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
( LBound B1,X in X & B1 in LBound B1,X )
let B1 be Ordinal; :: thesis: for X being Subset of A st X is unbounded & B1 in A holds
( LBound B1,X in X & B1 in LBound B1,X )
let X be Subset of A; :: thesis: ( X is unbounded & B1 in A implies ( LBound B1,X in X & B1 in LBound B1,X ) )
assume A1: X is unbounded ; :: thesis: ( not B1 in A or ( LBound B1,X in X & B1 in LBound B1,X ) )
assume A2: B1 in A ; :: thesis: ( LBound B1,X in X & B1 in LBound B1,X )
not X is empty by A1, Th8;
hence LBound B1,X in X ; :: thesis: B1 in LBound B1,X
defpred S₁[ set ] means ( $1 in X & B1 in $1 );
set LB = { B2 where B2 is Element of A : S₁[B2] } ;
A3: inf { B2 where B2 is Element of A : S₁[B2] } = meet (On { B2 where B2 is Element of A : S₁[B2] } ) by ORDINAL2:def 6;
{ B2 where B2 is Element of A : S₁[B2] } is Subset of A from DOMAIN_1:sch 7();
then A4: On { B2 where B2 is Element of A : S₁[B2] } = { B2 where B2 is Element of A : S₁[B2] } by ORDINAL3:8;
A5: ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S₁[B2] } by A1, A2, Th9;
for x being set st x in { B2 where B2 is Element of A : S₁[B2] } holds
B1 in x

proof

let x be set ; :: thesis: ( x in { B2 where B2 is Element of A : S₁[B2] } implies B1 in x )
assume A6: x in { B2 where B2 is Element of A : S₁[B2] } ; :: thesis: B1 in x
S₁[x] from CARD_FIL:sch 1(A6);
hence B1 in x ; :: thesis: verum

end;

then B1 in meet { B2 where B2 is Element of A : S₁[B2] } by A5, SETFAM_1:def 1;
hence B1 in LBound B1,X by A1, A2, A3, A4, Def6; :: thesis: verum