let E be non empty set ; :: thesis: ( E is epsilon-transitive implies for u, v being Element of E st ( for w being Element of E holds

( w in u iff w in v ) ) holds

u = v )

assume A1: for X being set st X in E holds

X c= E ; :: according to ORDINAL1:def 2 :: thesis: for u, v being Element of E st ( for w being Element of E holds

( w in u iff w in v ) ) holds

u = v

let u, v be Element of E; :: thesis: ( ( for w being Element of E holds

( w in u iff w in v ) ) implies u = v )

assume A2: for w being Element of E holds

( w in u iff w in v ) ; :: thesis: u = v

A3: u c= E by A1;

thus u c= v by A3, A2; :: according to XBOOLE_0:def 10 :: thesis: v c= u

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in v or a in u )

assume A4: a in v ; :: thesis: a in u

v c= E by A1;

then reconsider e = a as Element of E by A4;

e in u by A2, A4;

hence a in u ; :: thesis: verum

( w in u iff w in v ) ) holds

u = v )

assume A1: for X being set st X in E holds

X c= E ; :: according to ORDINAL1:def 2 :: thesis: for u, v being Element of E st ( for w being Element of E holds

( w in u iff w in v ) ) holds

u = v

let u, v be Element of E; :: thesis: ( ( for w being Element of E holds

( w in u iff w in v ) ) implies u = v )

assume A2: for w being Element of E holds

( w in u iff w in v ) ; :: thesis: u = v

A3: u c= E by A1;

thus u c= v by A3, A2; :: according to XBOOLE_0:def 10 :: thesis: v c= u

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in v or a in u )

assume A4: a in v ; :: thesis: a in u

v c= E by A1;

then reconsider e = a as Element of E by A4;

e in u by A2, A4;

hence a in u ; :: thesis: verum