defpred S₁[ set ] means $1 is OrderSortedSubset of M;
set f = product (bool M);
consider X being set such that
A1: for y being set holds
( y in X iff ( y in product (bool M) & S₁[y] ) ) from XFAMILY:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff x is OrderSortedSubset of M )
let y be set ; :: thesis: ( y in X iff y is OrderSortedSubset of M )
thus ( y in X implies y is OrderSortedSubset of M ) by A1; :: thesis: ( y is OrderSortedSubset of M implies y in X )
assume A2: y is OrderSortedSubset of M ; :: thesis: y in X
then y in product (bool M) by Th15;
hence y in X by A1, A2; :: thesis: verum