take Family_open_set ET ; :: thesis: ( Family_open_set ET is open & Family_open_set ET is quasi_basis )
thus ( Family_open_set ET is open & Family_open_set ET is quasi_basis ) ; :: thesis: verum