let V1, V2 be Subset of K; :: thesis: ( ( for v being Element of K holds
( v in V1 iff v is vertex-like ) ) & ( for v being Element of K holds
( v in V2 iff v is vertex-like ) ) implies V1 = V2 )
assume that
A3: for v being Element of K holds
( v in V1 iff v is vertex-like ) and
A4: for v being Element of K holds
( v in V2 iff v is vertex-like ) ; :: thesis: V1 = V2

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: V2 c= V1

let x be set ; :: thesis: ( x in V1 implies x in V2 )
assume A5: x in V1 ; :: thesis: x in V2
then reconsider v = x as Element of K ;
v is vertex-like by A3, A5;
hence x in V2 by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in V2 or x in V1 )
assume A6: x in V2 ; :: thesis: x in V1
then reconsider v = x as Element of K ;
v is vertex-like by A4, A6;
hence x in V1 by A3; :: thesis: verum