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 2, ORDINAL3:6;
assume A5: B1 in A ; :: thesis: ( LBound (B1,X) in X & B1 in LBound (B1,X) )
not X is empty by A1, Th7;
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, Th8;
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