let i be object ; :: according to PBOOLE:def 13 :: 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