let x1 be set ; :: according to INTEGRA1:def 4 :: thesis: ( x1 in divs A iff x1 is DivisionPoint of A )
thus ( x1 in divs A iff x1 is DivisionPoint of A ) by Def3; :: thesis: verum