let X be set ; :: thesis: ( ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) implies ( X is epsilon-transitive & X is epsilon-connected ) )
assume A1: for x being set st x in X holds
( x is Ordinal & x c= X ) ; :: thesis: ( X is epsilon-transitive & X is epsilon-connected )
thus X is epsilon-transitive by A1; :: thesis: X is epsilon-connected
let x be set ; :: according to ORDINAL1:def 3 :: thesis: for y being set st x in X & y in X & not x in y & not x = y holds
y in x
let y be set ; :: thesis: ( x in X & y in X & not x in y & not x = y implies y in x )
assume ( x in X & y in X ) ; :: thesis: ( x in y or x = y or y in x )
then ( x is Ordinal & y is Ordinal ) by A1;
hence ( x in y or x = y or y in x ) by Th10; :: thesis: verum