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 )
assume A1: X is closed_wrt_A1-A7 ; :: thesis: {} in X
consider o being Element of X;
reconsider p = o as Element of V ;
A2: {p} in X by A1, Th2;
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} ) } ;
A3: X is closed_wrt_A1 by A1, Def13;

now

assume A4: { {[(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
consider q being 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} ) } ;
q 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} ) } by A4;
then consider x, y being Element of V such that
A5: ( q = {[(0-element_of V),x],[(1-element_of V),y]} & x in y & x in {p} & y in {p} ) ;
( x = p & y = p ) by A5, TARSKI:def 1;
hence contradiction by A5; :: thesis: verum

end;

hence {} in X by A2, A3, Def6; :: thesis: verum