let X, Y be set ; :: thesis: for U being Universe st X in U & Y in U holds
( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )
let U be Universe; :: thesis: ( X in U & Y in U implies ( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U ) )
assume A1: ( X in U & Y in U ) ; :: thesis: ( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )
then ( {X,Y} in U & union {X,Y} = X \/ Y & meet {X,Y} = X /\ Y ) by Th3, SETFAM_1:12, ZFMISC_1:93;
hence A2: ( X \/ Y in U & X /\ Y in U ) by Th65; :: thesis: ( X \ Y in U & X \+\ Y in U )
( X \ Y c= X & X \+\ Y = (X \/ Y) \ (X /\ Y) & (X \/ Y) \ (X /\ Y) c= X \/ Y ) by XBOOLE_1:101;
hence ( X \ Y in U & X \+\ Y in U ) by A1, A2, CLASSES1:def 1; :: thesis: verum