let X, Y be set ; :: thesis: for U being Universe st X in U & Y in U holds
( [:X,Y:] in U & Funcs X,Y in U )
let U be Universe; :: thesis: ( X in U & Y in U implies ( [:X,Y:] in U & Funcs X,Y in U ) )
assume ( X in U & Y in U ) ; :: thesis: ( [:X,Y:] in U & Funcs X,Y in U )
then X \/ Y in U by Th66;
then bool (X \/ Y) in U by Th65;
then ( [:X,Y:] c= bool (bool (X \/ Y)) & bool (bool (X \/ Y)) in U ) by Th65, ZFMISC_1:105;
hence [:X,Y:] in U by CLASSES1:def 1; :: thesis: Funcs X,Y in U
then ( bool [:X,Y:] in U & Funcs X,Y c= bool [:X,Y:] ) by Th65, FRAENKEL:5;
hence Funcs X,Y in U by CLASSES1:def 1; :: thesis: verum