let V be Universe; :: thesis: for X being Subclass of V st X is closed_wrt_A1-A7 holds
{} in X
let X be Subclass of V; :: thesis: ( X is closed_wrt_A1-A7 implies {} in X )
set o = the Element of X;
reconsider p = the Element of X as Element of V ;
set D = { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } ;

A1: now :: thesis: not { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } <> {}

set q = the Element of { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } ;
assume { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } <> {} ; :: thesis: contradiction
then the Element of { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } in { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } ;
then consider x, y being Element of V such that
the Element of { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } = {[(0-element_of V),x],[(1-element_of V),y]} and
A2: x in y and
A3: ( x in {p} & y in {p} ) ;
( x = p & y = p ) by A3, TARSKI:def 1;
hence contradiction by A2; :: thesis: verum

end;

assume X is closed_wrt_A1-A7 ; :: thesis: {} in X
then ( {p} in X & X is closed_wrt_A1 ) by Th2;
hence {} in X by A1; :: thesis: verum