set F1 = { (rng x) where x is Element of X : x in X } ;
set F2 = { (rng x) where x is Element of X \/ {{}} : x in X } ;
X null {{}} c= X \/ {{}} ;
then A1: X c= X \/ {{}} ;
{ (rng x) where x is Element of X : x in X } = { (rng x) where x is Element of X \/ {{}} : x in X } from FOMODEL0:sch 1(A1);
hence for b₁ being set holds
( b₁ = SymbolsOf X iff b₁ = union { (rng x) where x is Element of X : x in X } ) ; :: thesis: verum