let L be non empty RelStr ; :: thesis: ( [#] L is infs-closed & [#] L is sups-closed )

for X being Subset of ([#] L) st ex_inf_of X,L holds

"/\" (X,L) in [#] L ;

hence [#] L is infs-closed by WAYBEL23:19; :: thesis: [#] L is sups-closed

for X being Subset of ([#] L) st ex_sup_of X,L holds

"\/" (X,L) in [#] L ;

hence [#] L is sups-closed by WAYBEL23:20; :: thesis: verum

for X being Subset of ([#] L) st ex_inf_of X,L holds

"/\" (X,L) in [#] L ;

hence [#] L is infs-closed by WAYBEL23:19; :: thesis: [#] L is sups-closed

for X being Subset of ([#] L) st ex_sup_of X,L holds

"\/" (X,L) in [#] L ;

hence [#] L is sups-closed by WAYBEL23:20; :: thesis: verum