let S be GraphUnionSet; :: thesis: for G being GraphUnion of S
for e, v, w being object st e Joins v,w,G holds
ex H being Element of S st e Joins v,w,H
let G be GraphUnion of S; :: thesis: for e, v, w being object st e Joins v,w,G holds
ex H being Element of S st e Joins v,w,H
let e, v, w be object ; :: thesis: ( e Joins v,w,G implies ex H being Element of S st e Joins v,w,H )
assume e Joins v,w,G ; :: thesis: ex H being Element of S st e Joins v,w,H
per cases then ( e DJoins v,w,G or e DJoins w,v,G ) by GLIB_000:16;
suppose e DJoins v,w,G ; :: thesis: ex H being Element of S st e Joins v,w,H
then consider H being Element of S such that
A1: e DJoins v,w,H by Th119;
take H ; :: thesis: e Joins v,w,H
thus e Joins v,w,H by A1, GLIB_000:16; :: thesis: verum
end;
suppose e DJoins w,v,G ; :: thesis: ex H being Element of S st e Joins v,w,H
then consider H being Element of S such that
A2: e DJoins w,v,H by Th119;
take H ; :: thesis: e Joins v,w,H
thus e Joins v,w,H by A2, GLIB_000:16; :: thesis: verum
end;
end;