let X, Y be set ; 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; ( 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
; ( 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; ( 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; verum