set X = the non empty finite set ;
TopSpaceMetr (DiscreteSpace the non empty finite set ) is finite ;
hence ex b₁ being non empty TopSpace st
( b₁ is Lindelof & b₁ is metrizable ) ; :: thesis: verum