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