take TrapezoidalFS (0,1,2,3) ; :: thesis: TrapezoidalFS (0,1,2,3) is trapezoidal
thus TrapezoidalFS (0,1,2,3) is trapezoidal ; :: thesis: verum