defpred S_{1}[ set ] means ex A1 being Subset of GX st

( A1 = $1 & A1 is connected & V c= $1 );

consider F being Subset-Family of GX such that

A1: for A being Subset of GX holds

( A in F iff S_{1}[A] )
from SUBSET_1:sch 3();

take union F ; :: thesis: ex F being Subset-Family of GX st

( ( for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )

take F ; :: thesis: ( ( for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )

thus for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) :: thesis: union F = union F

( A1 = $1 & A1 is connected & V c= $1 );

consider F being Subset-Family of GX such that

A1: for A being Subset of GX holds

( A in F iff S

take union F ; :: thesis: ex F being Subset-Family of GX st

( ( for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )

take F ; :: thesis: ( ( for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )

thus for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) :: thesis: union F = union F

proof

thus
union F = union F
; :: thesis: verum
let A be Subset of GX; :: thesis: ( A in F iff ( A is connected & V c= A ) )

thus ( A in F implies ( A is connected & V c= A ) ) :: thesis: ( A is connected & V c= A implies A in F )

end;thus ( A in F implies ( A is connected & V c= A ) ) :: thesis: ( A is connected & V c= A implies A in F )

proof

thus
( A is connected & V c= A implies A in F )
by A1; :: thesis: verum
assume
A in F
; :: thesis: ( A is connected & V c= A )

then ex A1 being Subset of GX st

( A1 = A & A1 is connected & V c= A ) by A1;

hence ( A is connected & V c= A ) ; :: thesis: verum

end;then ex A1 being Subset of GX st

( A1 = A & A1 is connected & V c= A ) by A1;

hence ( A is connected & V c= A ) ; :: thesis: verum