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 ) )_{1} being Subset-Family of ET st b_{1} is quasi_basis
; :: thesis: verum

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

hence
ex b
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 ) )

thus x in OP by A2, Th9; :: thesis: verum

end;( 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 )

given Y being Subset-Family of ET such that A2:
( Y c= OP & x = union Y )
; :: thesis: x in OP( 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;( 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

thus x in OP by A2, Th9; :: thesis: verum