e in { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;
then consider e1 being Element of SubSort OU0 such that
A1: ( e = e1 & e1 is OrderSortedSet of S1 ) ;
reconsider e2 = @ e1 as OSSubset of OU0 by A1, Def2;
e2 = e by A1;
hence e is OSSubset of OU0 ; :: thesis: verum