take Family_open_set ET ; :: thesis: Family_open_set ET is open
thus Family_open_set ET is open ; :: thesis: verum