let S1, S2 be GraphUnionSet; :: thesis: for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st S2 c= S1 holds
G2 is Subgraph of G1
let G1 be GraphUnion of S1; :: thesis: for G2 being GraphUnion of S2 st S2 c= S1 holds
G2 is Subgraph of G1
let G2 be GraphUnion of S2; :: thesis: ( S2 c= S1 implies G2 is Subgraph of G1 )
assume A1: S2 c= S1 ; :: thesis: G2 is Subgraph of G1
now :: thesis: for H2 being Element of S2 ex H1 being Element of S1 st H2 is Subgraph of H1
let H2 be Element of S2; :: thesis: ex H1 being Element of S1 st H2 is Subgraph of H1
reconsider H1 = H2 as Element of S1 by A1, TARSKI:def 3;
take H1 = H1; :: thesis: H2 is Subgraph of H1
thus H2 is Subgraph of H1 by GLIB_000:40; :: thesis: verum
end;
hence G2 is Subgraph of G1 by Th121; :: thesis: verum