defpred S₁[ set ] means ex A1 being Subset of st
( A1 = $1 & A1 is connected & V c= $1 );
consider F being Subset-Family of such that
A1: for A being Subset of holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
take union F ; :: thesis: ex F being Subset-Family of st
( ( for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )
take F ; :: thesis: ( ( for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = union F )
thus for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) :: thesis: union F = union F

proof

let A be Subset of ; :: 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 )

proof

assume A in F ; :: thesis: ( A is connected & V c= A )
then ex A1 being Subset of st
( A1 = A & A1 is connected & V c= A ) by A1;
hence ( A is connected & V c= A ) ; :: thesis: verum

end;

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

end;

thus union F = union F ; :: thesis: verum