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