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 that
A1: X in U and
A2: Y in U ; :: thesis: ( [:X,Y:] in U & Funcs X,Y in U )
X \/ Y in U by A1, A2, Th66;
then bool (X \/ Y) in U by Th65;
then A3: bool (bool (X \/ Y)) in U by Th65;
[:X,Y:] c= bool (bool (X \/ Y)) by ZFMISC_1:105;
hence [:X,Y:] in U by A3, CLASSES1:def 1; :: thesis: Funcs X,Y in U
then A4: bool [:X,Y:] in U by Th65;
Funcs X,Y c= bool [:X,Y:] by FRAENKEL:5;
hence Funcs X,Y in U by A4, CLASSES1:def 1; :: thesis: verum