let I be set ; :: thesis: for X, Y being ManySortedSet of I st X is V8() & X [= Y holds
Y is V8()
let X, Y be ManySortedSet of I; :: thesis: ( X is V8() & X [= Y implies Y is V8() )
assume A1: X is V8() ; :: thesis: ( not X [= Y or not Y is V8() )
assume X [= Y ; :: thesis: Y is V8()
then X c= Y by A1, Th132;
hence Y is V8() by A1, Th131; :: thesis: verum