take divs A ; :: thesis: for x1 being set holds
( x1 in divs A iff x1 is DivisionPoint of A )
thus for x1 being set holds
( x1 in divs A iff x1 is DivisionPoint of A ) by Def3; :: thesis: verum