let x1, x2 be Subset of [:NAT,NAT:]; :: thesis: ( ( for x being Element of [:NAT,NAT:] holds

( x in x1 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) & ( for x being Element of [:NAT,NAT:] holds

( x in x2 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) implies x1 = x2 )

assume that

A1: for x being Element of [:NAT,NAT:] holds

( x in x1 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) and

A2: for x being Element of [:NAT,NAT:] holds

( x in x2 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ; :: thesis: x1 = x2

thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis: x2 c= x1

assume A4: t in x2 ; :: thesis: t in x1

then reconsider u = t as Element of [:NAT,NAT:] ;

ex n1, n2 being Nat st

( n1 = u `1 & n2 = u `2 & n1 < n & n2 < n ) by A4, A2;

hence t in x1 by A1; :: thesis: verum

( x in x1 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) & ( for x being Element of [:NAT,NAT:] holds

( x in x2 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) implies x1 = x2 )

assume that

A1: for x being Element of [:NAT,NAT:] holds

( x in x1 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) and

A2: for x being Element of [:NAT,NAT:] holds

( x in x2 iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ; :: thesis: x1 = x2

thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis: x2 c= x1

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x2 or t in x1 )
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x1 or t in x2 )

assume A3: t in x1 ; :: thesis: t in x2

then reconsider u = t as Element of [:NAT,NAT:] ;

ex n1, n2 being Nat st

( n1 = u `1 & n2 = u `2 & n1 < n & n2 < n ) by A3, A1;

hence t in x2 by A2; :: thesis: verum

end;assume A3: t in x1 ; :: thesis: t in x2

then reconsider u = t as Element of [:NAT,NAT:] ;

ex n1, n2 being Nat st

( n1 = u `1 & n2 = u `2 & n1 < n & n2 < n ) by A3, A1;

hence t in x2 by A2; :: thesis: verum

assume A4: t in x2 ; :: thesis: t in x1

then reconsider u = t as Element of [:NAT,NAT:] ;

ex n1, n2 being Nat st

( n1 = u `1 & n2 = u `2 & n1 < n & n2 < n ) by A4, A2;

hence t in x1 by A1; :: thesis: verum