reconsider OP = Family_open_set ET as Subset-Family of ET ;
for x being Subset of ET holds
( x in OP iff ex Y being Subset-Family of ET st
( Y c= OP & x = union Y ) )

proof

let x be Subset of ET; :: thesis: ( x in OP iff ex Y being Subset-Family of ET st
( Y c= OP & x = union Y ) )

hereby :: thesis: ( ex Y being Subset-Family of ET st
( Y c= OP & x = union Y ) implies x in OP )

assume A1: x in OP ; :: thesis: ex Y being Subset-Family of ET st
( Y c= OP & x = union Y )
reconsider B = {x} as Subset-Family of ET ;
x = union B ;
hence ex Y being Subset-Family of ET st
( Y c= OP & x = union Y ) by A1, ZFMISC_1:31; :: thesis: verum

end;

given Y being Subset-Family of ET such that A2: ( Y c= OP & x = union Y ) ; :: thesis: x in OP
thus x in OP by A2, Th9; :: thesis: verum

end;

hence ex b₁ being Subset-Family of ET st b₁ is quasi_basis ; :: thesis: verum