let A be limit_ordinal infinite Ordinal; 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; 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; ( X is unbounded & B1 in A implies ( LBound (B1,X) in X & B1 in LBound (B1,X) ) )
assume A1:
X is unbounded
; ( not B1 in A or ( LBound (B1,X) in X & B1 in LBound (B1,X) ) )
defpred S1[ set ] means ( $1 in X & B1 in $1 );
set LB = { B2 where B2 is Element of A : S1[B2] } ;
A2:
for x being set st x in { B2 where B2 is Element of A : S1[B2] } holds
B1 in x
{ B2 where B2 is Element of A : S1[B2] } is Subset of A
from DOMAIN_1:sch 7();
then A4:
( inf { B2 where B2 is Element of A : S1[B2] } = meet (On { B2 where B2 is Element of A : S1[B2] } ) & On { B2 where B2 is Element of A : S1[B2] } = { B2 where B2 is Element of A : S1[B2] } )
by ORDINAL2:def 2, ORDINAL3:6;
assume A5:
B1 in A
; ( LBound (B1,X) in X & B1 in LBound (B1,X) )
not X is empty
by A1, Th7;
hence
LBound (B1,X) in X
; B1 in LBound (B1,X)
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S1[B2] }
by A1, A5, Th8;
then
B1 in meet { B2 where B2 is Element of A : S1[B2] }
by A2, SETFAM_1:def 1;
hence
B1 in LBound (B1,X)
by A1, A5, A4, Def6; verum