let X, Y be non empty TopSpace; :: thesis: for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 X,Y) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 the carrier of X,the carrier of Y) .: D )
let H be Subset-Family of [:X,Y:]; :: thesis: for C being set st C in (Pr1 X,Y) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 the carrier of X,the carrier of Y) .: D )
let C be set ; :: thesis: ( C in (Pr1 X,Y) .: H implies ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 the carrier of X,the carrier of Y) .: D ) )
A1: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by Def5;
assume C in (Pr1 X,Y) .: H ; :: thesis: ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 the carrier of X,the carrier of Y) .: D )
then consider u being set such that
A2: ( u in dom (Pr1 X,Y) & u in H & C = (Pr1 X,Y) . u ) by FUNCT_1:def 12;
reconsider u = u as Subset of [:X,Y:] by A2;
take u ; :: thesis: ( u in H & C = (pr1 the carrier of X,the carrier of Y) .: u )
thus u in H by A2; :: thesis: C = (pr1 the carrier of X,the carrier of Y) .: u
thus C = (pr1 the carrier of X,the carrier of Y) .: u by A1, A2, Th9; :: thesis: verum