( the carrier of (X /==) = the carrier of X & the carrier' of (X /==) = Class (==_ X) ) by Def20;
hence ( not X /== is empty & not X /== is void ) ; :: thesis: verum