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

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