defpred S₁[ object ] means ex H being Subgroup of F₁() st
( $1 = H & P₁[H] );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in Subgroups F₁() & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: ( X c= Subgroups F₁() & ( for H being strict Subgroup of F₁() holds
( H in X iff P₁[H] ) ) )
thus X c= Subgroups F₁() by A1; :: thesis: for H being strict Subgroup of F₁() holds
( H in X iff P₁[H] )
let H be strict Subgroup of F₁(); :: thesis: ( H in X iff P₁[H] )
thus ( H in X implies P₁[H] ) :: thesis: ( P₁[H] implies H in X )

proof

assume H in X ; :: thesis: P₁[H]
then ex H1 being Subgroup of F₁() st
( H = H1 & P₁[H1] ) by A1;
hence P₁[H] ; :: thesis: verum

end;

A2: H in Subgroups F₁() by GROUP_3:def 1;
assume P₁[H] ; :: thesis: H in X
hence H in X by A1, A2; :: thesis: verum