let L be RelStr ; :: thesis: for x being set holds
( x is lower Subset of iff x is upper Subset of )
let x be set ; :: thesis: ( x is lower Subset of iff x is upper Subset of )
( x is upper Subset of iff x is upper Subset of ) by WAYBEL_0:25;
hence ( x is lower Subset of iff x is upper Subset of ) by Th28; :: thesis: verum