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 and
A2: e1 is OrderSortedSet of S1 ;
reconsider e2 = @ e1 as OSSubset of OU0 by A2, Def2;
e2 = e by A1;
hence e is OSSubset of OU0 ; :: thesis: verum