now :: thesis: for x being object st x in { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } holds
x in G .allSG()

let x be object ; :: thesis: ( x in { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } implies x in G .allSG() )
assume x in { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } ; :: thesis: x in G .allSG()
then consider H being Element of [#] (G .allSG()) such that
A1: x = H and
( H is spanning & H is acyclic ) ;
thus x in G .allSG() by A1; :: thesis: verum

end;

hence { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } is Subset of (G .allSG()) by TARSKI:def 3; :: thesis: verum