let G be _Graph; :: thesis: SubgraphRel G partially_orders G .allSG()

now :: thesis: for x being object st x in G .allSG() holds
[x,x] in SubgraphRel G

let x be object ; :: thesis: ( x in G .allSG() implies [x,x] in SubgraphRel G )
assume x in G .allSG() ; :: thesis: [x,x] in SubgraphRel G
then reconsider H = x as Element of G .allSG() ;
H is Subgraph of H by GLIB_000:40;
hence [x,x] in SubgraphRel G by Def6; :: thesis: verum

end;

then A1: SubgraphRel G is_reflexive_in G .allSG() by RELAT_2:def 1;

now :: thesis: for x, y being object st x in G .allSG() & y in G .allSG() & [x,y] in SubgraphRel G & [y,x] in SubgraphRel G holds
x = y

let x, y be object ; :: thesis: ( x in G .allSG() & y in G .allSG() & [x,y] in SubgraphRel G & [y,x] in SubgraphRel G implies x = y )
assume that
A2: ( x in G .allSG() & y in G .allSG() ) and
A3: ( [x,y] in SubgraphRel G & [y,x] in SubgraphRel G ) ; :: thesis: x = y
reconsider H1 = x, H2 = y as Element of G .allSG() by A2;
( H1 is Subgraph of H2 & H2 is Subgraph of H1 ) by A3, Def6;
hence x = y by GLIB_000:87, GLIB_009:44; :: thesis: verum

end;

then A4: SubgraphRel G is_antisymmetric_in G .allSG() by RELAT_2:def 4;

now :: thesis: for x, y, z being object st x in G .allSG() & y in G .allSG() & z in G .allSG() & [x,y] in SubgraphRel G & [y,z] in SubgraphRel G holds
[x,z] in SubgraphRel G

let x, y, z be object ; :: thesis: ( x in G .allSG() & y in G .allSG() & z in G .allSG() & [x,y] in SubgraphRel G & [y,z] in SubgraphRel G implies [x,z] in SubgraphRel G )
assume that
A5: ( x in G .allSG() & y in G .allSG() & z in G .allSG() ) and
A6: ( [x,y] in SubgraphRel G & [y,z] in SubgraphRel G ) ; :: thesis: [x,z] in SubgraphRel G
reconsider H1 = x, H2 = y, H3 = z as Element of G .allSG() by A5;
( H1 is Subgraph of H2 & H2 is Subgraph of H3 ) by A6, Def6;
then H1 is Subgraph of H3 by GLIB_000:43;
hence [x,z] in SubgraphRel G by Def6; :: thesis: verum

end;

hence SubgraphRel G partially_orders G .allSG() by A1, A4, RELAT_2:def 8, ORDERS_1:def 8; :: thesis: verum