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 that
A1: X in U and
A2: Y in U ; :: thesis: ( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )
A3: union {X,Y} = X \/ Y by ZFMISC_1:75;
A4: meet {X,Y} = X /\ Y by SETFAM_1:11;
{X,Y} in U by A1, A2, Th2;
hence A5: ( X \/ Y in U & X /\ Y in U ) by A3, A4, Th59; :: thesis: ( X \ Y in U & X \+\ Y in U )
X \+\ Y = (X \/ Y) \ (X /\ Y) by XBOOLE_1:101;
hence ( X \ Y in U & X \+\ Y in U ) by A1, A5, CLASSES1:def 1; :: thesis: verum