let A1, A2 be Subset of (Vertices G); :: thesis: ( ( for x being Element of Vertices G holds
( x in A1 iff {v,x} in Edges G ) ) & ( for x being Element of Vertices G holds
( x in A2 iff {v,x} in Edges G ) ) implies A1 = A2 )
assume that
A5: for x being Element of Vertices G holds
( x in A1 iff {v,x} in Edges G ) and
A6: for x being Element of Vertices G holds
( x in A2 iff {v,x} in Edges G ) ; :: thesis: A1 = A2
thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in A2 )
assume A7: x in A1 ; :: thesis: x in A2
then {v,x} in Edges G by A5;
hence x in A2 by A6, A7; :: thesis: verum

end;

thus A2 c= A1 :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A2 or x in A1 )
assume A8: x in A2 ; :: thesis: x in A1
then {v,x} in Edges G by A6;
hence x in A1 by A5, A8; :: thesis: verum

end;