defpred S1[ set ] means ex A1 being Subset of X st
( A1 = \$1 & A1 is open & A1 is closed & x in \$1 );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S1[A] ) from reconsider S = meet F as Subset of X ;
take S ; :: thesis: ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S )

take F ; :: thesis: ( ( for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S )

thus for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) :: thesis: meet F = S
proof
let A be Subset of X; :: thesis: ( A in F iff ( A is open & A is closed & x in A ) )
thus ( A in F implies ( A is open & A is closed & x in A ) ) :: thesis: ( A is open & A is closed & x in A implies A in F )
proof
assume A in F ; :: thesis: ( A is open & A is closed & x in A )
then ex A1 being Subset of X st
( A1 = A & A1 is open & A1 is closed & x in A ) by A1;
hence ( A is open & A is closed & x in A ) ; :: thesis: verum
end;
thus ( A is open & A is closed & x in A implies A in F ) by A1; :: thesis: verum
end;
thus meet F = S ; :: thesis: verum