set c = { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } ;
{ x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } c= F2() -polytopes F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } or x in F2() -polytopes F1() )
assume x in { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } ; :: thesis: x in F2() -polytopes F1()
then ex y being Element of F2() -polytopes F1() st
( x = y & P1[y] & y in F2() -polytopes F1() ) ;
hence x in F2() -polytopes F1() ; :: thesis: verum
end;
then reconsider c = { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } as Subset of (F2() -polytopes F1()) ;
take c ; :: thesis: for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
proof
let x be Element of F2() -polytopes F1(); :: thesis: ( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
thus ( x in c implies ( P1[x] & x in F2() -polytopes F1() ) ) :: thesis: ( P1[x] & x in F2() -polytopes F1() implies x in c )
proof
assume x in c ; :: thesis: ( P1[x] & x in F2() -polytopes F1() )
then ex y being Element of F2() -polytopes F1() st
( y = x & P1[y] & y in F2() -polytopes F1() ) ;
hence ( P1[x] & x in F2() -polytopes F1() ) ; :: thesis: verum
end;
thus ( P1[x] & x in F2() -polytopes F1() implies x in c ) ; :: thesis: verum
end;
hence for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) ) ; :: thesis: verum