:: deftheorem Def2 defines Sub WAYBEL10:def 2 :
for L being RelStr
for b₂ being non empty strict RelStr holds
( b₂ = Sub L iff ( ( for x being object holds
( x is Element of b₂ iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b₂ holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) ) );