let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in the carrier of (X -CircuitStr ) or not (X -CircuitSorts A) . i is empty )
assume i in the carrier of (X -CircuitStr ) ; :: thesis: not (X -CircuitSorts A) . i is empty
then reconsider i = i as Vertex of (X -CircuitStr ) ;
(X -CircuitSorts A) . i = the_sort_of i,A by Def4;
hence not (X -CircuitSorts A) . i is empty ; :: thesis: verum