let L be non empty RelStr ; :: thesis: ( [#] L is with_bottom & [#] L is with_top )
Bottom L in [#] L ;
hence [#] L is with_bottom by WAYBEL23:def 8; :: thesis: [#] L is with_top
Top L in [#] L ;
hence [#] L is with_top by WAYBEL23:def 9; :: thesis: verum