consider X being set such that
A1: for x being object holds
( x in X iff ( x in bool F1() & P1[x] ) ) from XBOOLE_0:sch 1();
 take X ; :: thesis: for x being set holds
( x in X iff ( x is strict Subgraph of F1() & P1[x] ) )
let x be set ; :: thesis: ( x in X iff ( x is strict Subgraph of F1() & P1[x] ) )
thus ( x in X implies ( x is strict Subgraph of F1() & P1[x] ) ) :: thesis: ( x is strict Subgraph of F1() & P1[x] implies x in X )
proof
assume A2: x in X ; :: thesis: ( x is strict Subgraph of F1() & P1[x] )
then x in bool F1() by A1;
hence x is strict Subgraph of F1() by Def25; :: thesis: P1[x]
thus P1[x] by A1, A2; :: thesis: verum
end;
assume that
A3: x is strict Subgraph of F1() and
A4: P1[x] ; :: thesis: x in X
x in bool F1() by A3, Def25;
hence x in X by A1, A4; :: thesis: verum