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_{1}[ set ] means ( $1 in X & B1 in $1 );

set LB = { B2 where B2 is Element of A : S_{1}[B2] } ;

A2: for x being set st x in { B2 where B2 is Element of A : S_{1}[B2] } holds

B1 in x_{1}[B2] } is Subset of A
from DOMAIN_1:sch 7();

then A4: ( inf { B2 where B2 is Element of A : S_{1}[B2] } = meet (On { B2 where B2 is Element of A : S_{1}[B2] } ) & On { B2 where B2 is Element of A : S_{1}[B2] } = { B2 where B2 is Element of A : S_{1}[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_{1}[B2] }
by A1, A5, Th8;

then B1 in meet { B2 where B2 is Element of A : S_{1}[B2] }
by A2, SETFAM_1:def 1;

hence B1 in LBound (B1,X) by A1, A5, A4, Def6; :: thesis: verum

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 LB = { B2 where B2 is Element of A : S

A2: for x being set st x in { B2 where B2 is Element of A : S

B1 in x

proof

{ B2 where B2 is Element of A : S
let x be set ; :: thesis: ( x in { B2 where B2 is Element of A : S_{1}[B2] } implies B1 in x )

assume A3: x in { B2 where B2 is Element of A : S_{1}[B2] }
; :: thesis: B1 in x

S_{1}[x]
from CARD_FIL:sch 1(A3);

hence B1 in x ; :: thesis: verum

end;assume A3: x in { B2 where B2 is Element of A : S

S

hence B1 in x ; :: thesis: verum

then A4: ( inf { B2 where B2 is Element of A : S

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

then B1 in meet { B2 where B2 is Element of A : S

hence B1 in LBound (B1,X) by A1, A5, A4, Def6; :: thesis: verum