let x, y be set ; :: thesis: ( x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & not x c= y implies y c= x )
assume x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; :: thesis: ( not y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } or x c= y or y c= x )
then consider A' being Subset of RAT+ such that
A1: x = A' and
A2: for r being Element of RAT+ st r in A' holds
( ( for s being Element of RAT+ st s <=' r holds
s in A' ) & ex s being Element of RAT+ st
( s in A' & r < s ) ) ;
assume y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; :: thesis: ( x c= y or y c= x )
then consider B' being Subset of RAT+ such that
A3: y = B' and
A4: for r being Element of RAT+ st r in B' holds
( ( for s being Element of RAT+ st s <=' r holds
s in B' ) & ex s being Element of RAT+ st
( s in B' & r < s ) ) ;
assume not x c= y ; :: thesis: y c= x
then consider s being set such that
A5: s in x and
A6: not s in y by TARSKI:def 3;
reconsider s = s as Element of RAT+ by A1, A5;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in y or e in x )
assume A7: e in y ; :: thesis: e in x
then reconsider r = e as Element of RAT+ by A3;
r <=' s by A3, A4, A6, A7;
hence e in x by A1, A2, A5; :: thesis: verum