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 object 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 6;
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 Def2;
hence C = (pr1 ( the carrier of X, the carrier of Y)) .: u by A3, EQREL_1:47; :: thesis: verum