consider A being set such that
A3: for x being object holds
( x in A iff ( x in the carrier of F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
A c= the carrier of F₁() by A3;
then reconsider A = A as non empty Subset of F₁() by A1, A2, A3;
set S = subrelstr A;
take subrelstr A ; :: thesis: for x being Element of F₁() holds
( x is Element of (subrelstr A) iff P₁[x] )
let x be Element of F₁(); :: thesis: ( x is Element of (subrelstr A) iff P₁[x] )
A4: the carrier of (subrelstr A) = A by YELLOW_0:def 15;
hence ( x is Element of (subrelstr A) implies P₁[x] ) by A3; :: thesis: ( P₁[x] implies x is Element of (subrelstr A) )
assume P₁[x] ; :: thesis: x is Element of (subrelstr A)
hence x is Element of (subrelstr A) by A3, A4; :: thesis: verum