let X be set ; :: thesis: ( X is axiom_GU1 & X is axiom_GU3 implies ( ( for y being set
for x being Subset of y st y in X holds
x in X ) & ( for x, y being set st x c= y & y in X holds
x in X ) & ( not X is empty implies {} in X ) ) )
assume that
A1: for x, y being set st x in X & y in x holds
y in X and
A2: for x being set st x in X holds
bool x in X ; :: according to CLASSES4:def 1,CLASSES4:def 3 :: thesis: ( ( for y being set
for x being Subset of y st y in X holds
x in X ) & ( for x, y being set st x c= y & y in X holds
x in X ) & ( not X is empty implies {} in X ) )

A3: now :: thesis: for y being set
for x being Subset of y st y in X holds
x in X

let y be set ; :: thesis: for x being Subset of y st y in X holds
x in X
let x be Subset of y; :: thesis: ( y in X implies x in X )
assume y in X ; :: thesis: x in X
then bool y in X by A2;
hence x in X by A1; :: thesis: verum

end;

now :: thesis: ( not X is empty implies {} in X )

assume not X is empty ; :: thesis: {} in X
then consider x being object such that
A4: x in X ;
reconsider x9 = x as set by TARSKI:1;
{} c= x9 ;
hence {} in X by A4, A3; :: thesis: verum

end;

hence ( ( for y being set
for x being Subset of y st y in X holds
x in X ) & ( for x, y being set st x c= y & y in X holds
x in X ) & ( not X is empty implies {} in X ) ) by A3; :: thesis: verum