let V be non empty set ; :: thesis: for E being Relation of V holds (createGraph (V,E)) .loops() = E /\ (id V)
let E be Relation of V; :: thesis: (createGraph (V,E)) .loops() = E /\ (id V)
set G = createGraph (V,E);

now :: thesis: for x being object holds
( ( x in (createGraph (V,E)) .loops() implies ( x in E & x in id V ) ) & ( x in E & x in id V implies x in (createGraph (V,E)) .loops() ) )

let x be object ; :: thesis: ( ( x in (createGraph (V,E)) .loops() implies ( x in E & x in id V ) ) & ( x in E & x in id V implies x in (createGraph (V,E)) .loops() ) )

hereby :: thesis: ( x in E & x in id V implies x in (createGraph (V,E)) .loops() )

assume x in (createGraph (V,E)) .loops() ; :: thesis: ( x in E & x in id V )
then consider v being object such that
A1: x DJoins v,v, createGraph (V,E) by GLIB_009:45;
x Joins v,v, createGraph (V,E) by A1, GLIB_000:16;
then v in the_Vertices_of (createGraph (V,E)) by GLIB_000:13;
then A2: v in V ;
x = [v,v] by A1, GLUNIR00:64;
hence ( x in E & x in id V ) by A1, A2, GLUNIR00:63, RELAT_1:def 10; :: thesis: verum

end;

assume A3: ( x in E & x in id V ) ; :: thesis: x in (createGraph (V,E)) .loops()
then consider y, z being object such that
A4: x = [y,z] by RELAT_1:def 1;
x = [y,y] by A3, A4, RELAT_1:def 10;
hence x in (createGraph (V,E)) .loops() by A3, GLUNIR00:63, GLIB_009:45; :: thesis: verum

end;

hence (createGraph (V,E)) .loops() = E /\ (id V) by XBOOLE_0:def 4; :: thesis: verum