defpred S₁[ set ] means for G being Subset of GX st G is open & $1 in G holds
A meets G;
consider P being Subset of GX such that
A1: for x being set holds
( x in P iff ( x in the carrier of GX & S₁[x] ) ) from SUBSET_1:sch 1();
take P ; :: thesis: for p being set st p in the carrier of GX holds
( p in P iff for G being Subset of GX st G is open & p in G holds
A meets G )
thus for p being set st p in the carrier of GX holds
( p in P iff for G being Subset of GX st G is open & p in G holds
A meets G ) by A1; :: thesis: verum