let V be Universe; for X being Subclass of V st X is closed_wrt_A1-A7 holds
{} in X
let X be Subclass of V; ( 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 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} ) } <> {}
;
contradictionthen
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;
verum end;
assume
X is closed_wrt_A1-A7
; {} in X
then
( {p} in X & X is closed_wrt_A1 )
by Th2;
hence
{} in X
by A1; verum