consider X being set such that
A1: for x being object holds
( x in X iff ( x in bool F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ( x is strict Subgraph of F₁() & P₁[x] ) )
let x be set ; :: thesis: ( x in X iff ( x is strict Subgraph of F₁() & P₁[x] ) )
thus ( x in X implies ( x is strict Subgraph of F₁() & P₁[x] ) ) :: thesis: ( x is strict Subgraph of F₁() & P₁[x] implies x in X )

proof

assume A2: x in X ; :: thesis: ( x is strict Subgraph of F₁() & P₁[x] )
then x in bool F₁() by A1;
hence x is strict Subgraph of F₁() by Def25; :: thesis: P₁[x]
thus P₁[x] by A1, A2; :: thesis: verum

end;

assume that
A3: x is strict Subgraph of F₁() and
A4: P₁[x] ; :: thesis: x in X
x in bool F₁() by A3, Def25;
hence x in X by A1, A4; :: thesis: verum