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 ) )
defpred S₁[ set ] means ( $1 in X & B1 in $1 );
set LB = { B2 where B2 is Element of A : S₁[B2] } ;
A2: 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 A3: x in { B2 where B2 is Element of A : S₁[B2] } ; :: thesis: B1 in x
S₁[x] from CARD_FIL:sch 1(A3);
hence B1 in x ; :: thesis: verum

end;

{ B2 where B2 is Element of A : S₁[B2] } is Subset of A from DOMAIN_1:sch 7();
then A4: ( inf { B2 where B2 is Element of A : S₁[B2] } = meet (On { B2 where B2 is Element of A : S₁[B2] } ) & On { B2 where B2 is Element of A : S₁[B2] } = { B2 where B2 is Element of A : S₁[B2] } ) by ORDINAL2:def 6, ORDINAL3:8;
assume A5: 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
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S₁[B2] } by A1, A5, Th9;
then B1 in meet { B2 where B2 is Element of A : S₁[B2] } by A2, SETFAM_1:def 1;
hence B1 in LBound B1,X by A1, A5, A4, Def6; :: thesis: verum