set p = 1_. F_Complex;

take 1_. F_Complex ; :: thesis: ( not 1_. F_Complex is zero & 1_. F_Complex is real & 1_. F_Complex is positive )

thus not 1_. F_Complex is zero ; :: thesis: ( 1_. F_Complex is real & 1_. F_Complex is positive )

thus 1_. F_Complex is real ; :: thesis: 1_. F_Complex is positive

thus 1_. F_Complex is positive ; :: thesis: verum

take 1_. F_Complex ; :: thesis: ( not 1_. F_Complex is zero & 1_. F_Complex is real & 1_. F_Complex is positive )

thus not 1_. F_Complex is zero ; :: thesis: ( 1_. F_Complex is real & 1_. F_Complex is positive )

thus 1_. F_Complex is real ; :: thesis: 1_. F_Complex is positive

thus 1_. F_Complex is positive ; :: thesis: verum