set B0 = NonZero ();
set K1 = { p7 where p7 is Point of () : P1[p7] } ;
set K0 = { p where p is Point of () : ( P1[p] & p <> 0. () ) } ;
A1: { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ()) c= { p where p is Point of () : ( P1[p] & p <> 0. () ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ()) or x in { p where p is Point of () : ( P1[p] & p <> 0. () ) } )
assume A2: x in { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ()) ; :: thesis: x in { p where p is Point of () : ( P1[p] & p <> 0. () ) }
then x in NonZero () by XBOOLE_0:def 4;
then not x in {(0. ())} by XBOOLE_0:def 5;
then A3: x <> 0. () by TARSKI:def 1;
x in { p7 where p7 is Point of () : P1[p7] } by ;
then ex p7 being Point of () st
( p7 = x & P1[p7] ) ;
hence x in { p where p is Point of () : ( P1[p] & p <> 0. () ) } by A3; :: thesis: verum
end;
{ p where p is Point of () : ( P1[p] & p <> 0. () ) } c= { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : ( P1[p] & p <> 0. () ) } or x in { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ()) )
assume x in { p where p is Point of () : ( P1[p] & p <> 0. () ) } ; :: thesis: x in { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ())
then A4: ex p being Point of () st
( x = p & P1[p] & p <> 0. () ) ;
then not x in {(0. ())} by TARSKI:def 1;
then A5: x in NonZero () by ;
x in { p7 where p7 is Point of () : P1[p7] } by A4;
hence x in { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ()) by ; :: thesis: verum
end;
hence { p where p is Point of () : ( P1[p] & p <> 0. () ) } = { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ()) by A1; :: thesis: verum