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 & n <= n1 & n <= n2 ) ) ) & ( for x being Element of [:NAT,NAT:] holds
( x in x2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) 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 & n <= n1 & n <= n2 ) ) 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 & n <= n1 & n <= n2 ) ) ; :: thesis: x1 = x2
x1 = x2
proof
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 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 & n <= n1 & n <= n2 ) by A3, A1;
hence t in x2 by A2; :: thesis: verum
end;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x2 or t in 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 & n <= n1 & n <= n2 ) by A4, A2;
hence t in x1 by A1; :: thesis: verum
end;
hence x1 = x2 ; :: thesis: verum