let A be set ; :: thesis: ( A is preBoolean iff for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) )
thus ( A is preBoolean implies for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) ) by Def1, Def3; :: thesis: ( ( for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) ) implies A is preBoolean )
assume A1: for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) ; :: thesis: A is preBoolean
A2: A is diff-closed by A1;
A is cup-closed by A1;
hence A is preBoolean by A2; :: thesis: verum