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

proof

let X, Y be set ; :: according to FINSUB_1:def 3 :: thesis: ( X in A & Y in A implies X \ Y in A )
assume ( X in A & Y in A ) ; :: thesis: X \ Y in A
hence X \ Y in A by A1; :: thesis: verum

end;

A is cup-closed

proof

let X, Y be set ; :: according to FINSUB_1:def 1 :: thesis: ( X in A & Y in A implies X \/ Y in A )
assume ( X in A & Y in A ) ; :: thesis: X \/ Y in A
hence X \/ Y in A by A1; :: thesis: verum

end;

hence A is preBoolean by A2; :: thesis: verum