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