let X, Y be non empty TopSpace; :: thesis: for H being Subset-Family of [:X,Y:] st ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) holds
H = {}
let H be Subset-Family of [:X,Y:]; :: thesis: ( ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) implies H = {} )
( dom (Pr1 (X,Y)) = bool the carrier of [:X,Y:] & dom (Pr2 (X,Y)) = bool the carrier of [:X,Y:] ) by FUNCT_2:def 1;
hence ( ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) implies H = {} ) ; :: thesis: verum