let a be object ; :: thesis:
let A be Ordinal; :: thesis:
assume A1: a in A ; :: thesis:
reconsider a = a as set by TARSKI:1;
A2: a c= A by Def2, A1;

let y be set ; :: thesis:
assume A3: y in a ; :: thesis:
then A4: y c= A by A2, Def2;
assume not y c= a ; :: thesis:
then consider b being object such that
A5: ( b in y & not b in a ) ;
b in y \ a by A5, XBOOLE_0:def 5;
then consider z being set such that
A6: z in y \ a and
for c being object holds
( not c in y \ a or not c in z ) by TARSKI:3;
z in y by A6;
then ( z in a or z = a or a in z ) by A1, A4, Def3;
hence contradiction by A3, A6, XBOOLE_0:def 5, XREGULAR:7; :: thesis:

end;