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 ) )
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
A1: u in dom (Pr1 X,Y) and
A2: u in H and
A3: C = (Pr1 X,Y) . u by FUNCT_1:def 12;
reconsider u = u as Subset of [:X,Y:] by A1;
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
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by Def5;
hence C = (pr1 the carrier of X,the carrier of Y) .: u by A3, EQREL_1:56; :: thesis: verum