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

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